← all publishers

homeowmorphism

@homeowmorphism source repo

Report this profile Claim this profile

• 3 skills
• 0 followers
• 6 hours ago last updated

1. ▌
   Adaptive Teacher · homeowmorphism bundle

   General-purpose adaptive teaching, for any topic — mathematics, Lean, programming, or anything else. Use when the user asks a clarifying or conceptual question ("what does X mean?", "why does this work?", "what's the difference between X and Y?"), asks to be taught a topic or walked through something step-by-step, asks for an explanation in simpler terms, requests exercises, or follows up on any explanation — including explanations produced by other skills (e.g. mathlib-api). Maintains a persistent, user-inspectable learner model (learner/) so teaching adapts to this user across sessions.
   0
   installs
2. ▌
   Human Prose · homeowmorphism bundle

   Sentence-level readability rules for any prose a human will read — file comments, docstrings, module docs, commit messages, PR descriptions, chat explanations. Use when writing or rewriting such prose, when the user says text is dense, overwhelming, machine-written, or a long block of text, or when another skill's output needs a readability pass. Canonical home of this rule set; other skills point here rather than duplicating it.
   0
   installs
3. ▌
   Mathlib API · homeowmorphism bundle

   Evidence-driven workflow for designing a Mathlib definition and the API around it. Use when adding a new structure/def intended for mathlib; when choosing between design alternatives (index type as field vs parameter, Set vs indexed family, coarse set vs finer indexed structure and when the fine one should exist at all, data vs Prop, instance vs hypothesis, existential shape, `Nat.find` vs `sInf`-style encodings and where their classical plumbing lives, junk values of totalized quantities, sealed vs exposed bodies under the module system — `@[expose]`/`@[no_expose]` — and which object should carry an instance); when deciding which statements an API should ship and in what form (which Prop is the field, iff vs directional corollaries, simp orientation, smart constructors, bridges to existing idioms, bloat audits); when justifying a design in PR review; or when asked to "check the precedents" for a definition or an API, or to build a contrasting-cases example sheet. Clarifying and follow-up questions about a de
   0
   installs