From vibe-types
Lean 4 compile-time safety techniques — dependent types, inductive types, type classes, termination checking, propositions as types, proof automation. Use this skill whenever the user writes Lean 4 code, mentions dependent types, asks about theorem proving, discusses inductive types, type classes, tactics (simp, omega, decide), subtypes, termination proofs, or any Lean type system feature. Also use when formalizing invariants, writing proof-carrying code, or porting type patterns from Scala, Rust, or Haskell to Lean.
How this skill is triggered — by the user, by Claude, or both
Slash command
/vibe-types:leanThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
> **Base path:** `${CLAUDE_PLUGIN_ROOT}/skills/lean`
README.mdcatalog/00-overview.mdcatalog/T01-algebraic-data-types.mdcatalog/T02-union-intersection.mdcatalog/T03-newtypes-opaque.mdcatalog/T04-generics-bounds.mdcatalog/T05-type-classes.mdcatalog/T06-derivation.mdcatalog/T09-dependent-types.mdcatalog/T12-effect-tracking.mdcatalog/T13-null-safety.mdcatalog/T14-type-narrowing.mdcatalog/T15-const-generics.mdcatalog/T16-compile-time-ops.mdcatalog/T17-macros-metaprogramming.mdcatalog/T18-conversions-coercions.mdcatalog/T19-extension-methods.mdcatalog/T20-equality-safety.mdcatalog/T21-encapsulation.mdcatalog/T22-callable-typing.mdBase path:
${CLAUDE_PLUGIN_ROOT}/skills/lean
Inductive types & pattern matching — closed type hierarchies with exhaustive matching; compiler rejects incomplete matches → catalog/T01-algebraic-data-types.md
Dependent types & Pi types — return/field types depend on values; compiler checks index consistency → catalog/T09-dependent-types.md
Structures, inheritance, constructors — named-field product types with single-constructor guarantees; extends for inheritance → catalog/T31-record-types.md
Type classes & instance resolution — constrain generic functions to types with required capabilities → catalog/T05-type-classes.md
Universes & universe polymorphism — prevent type-in-type paradoxes; Sort u, Type u, Prop → catalog/T35-universes-kinds.md
Propositions as types (Prop) — encode invariants as Prop; compiler requires proof terms as evidence → catalog/T29-propositions-as-types.md
Termination & well-founded recursion — every recursive function must terminate; structural recursion or termination_by proof → catalog/T28-termination.md
Totality, partial functions — functions must handle all inputs; partial opts out but taints the result → catalog/T51-totality.md
Monads, do-notation, IO — side effects tracked via monadic types; IO demarcates impure computation → catalog/T12-effect-tracking.md
Coercions & Coe — automatic safe conversions between types; compiler inserts coercions where declared → catalog/T18-conversions-coercions.md
Auto-bound implicits & instances — compiler infers implicit arguments; [inst : C a] constrains to types with evidence → catalog/T38-implicits-auto-bound.md
Macros, elaboration, syntax — compile-time metaprogramming via syntax, macro_rules, and elab → catalog/T17-macros-metaprogramming.md
Proof automation (simp, decide, omega) — automate proof obligations; state what must hold, let tactics verify it → catalog/T30-proof-automation.md
Subtypes & refinement types — attach predicates to types ({ n : Nat // n > 0 }); construction requires proof → catalog/T26-refinement-types.md
Opaque definitions & reducibility — opaque def prevents unfolding outside the module; definitional encapsulation → catalog/T21-encapsulation.md
Notation, attributes, options — @[simp], @[inline], @[reducible] control how the checker treats definitions → catalog/T39-notation-attributes.md
Literal types — dependent types subsume literal types; any value can appear in a type via indexing → catalog/T52-literal-types.md
Path-dependent types — dependent types subsume path dependence; structures with type-valued fields → catalog/T53-path-dependent-types.md
Newtypes & opaque definitions — single-field structures, abbrev, opaque for hidden definitions → catalog/T03-newtypes-opaque.md
Null safety — no null in Lean; Option α is the standard pattern → catalog/T13-null-safety.md
Type narrowing — pattern matching narrows types; dependent match refines per branch → catalog/T14-type-narrowing.md
Compile-time computation — everything is compile-time; #eval, decide, simp, native_decide → catalog/T16-compile-time-ops.md
Equality safety — BEq/DecidableEq are opt-in; propositional vs boolean equality → catalog/T20-equality-safety.md
Callable typing — first-class functions, dependent function types, automatic currying → catalog/T22-callable-typing.md
Type aliases — abbrev (reducible), def (semireducible), opaque (irreducible) → catalog/T23-type-aliases.md
Erased types & Prop — Prop universe is erased at runtime; zero-cost proof evidence → catalog/T27-erased-phantom.md
Immutability — everything immutable by default; IO.Ref for controlled mutation → catalog/T32-immutability-markers.md
Empty & False — Empty type and False proposition; absurd for impossible cases → catalog/T34-never-bottom.md
Type lambdas — type-level functions are just functions; no special syntax needed → catalog/T40-type-lambdas.md
Match on types — dependent match works at the type level naturally → catalog/T41-match-types.md
Const generics (via dependent types) — dependent types subsume value-parameterized types → catalog/T15-const-generics.md
Union types (via inductives) — Sum α β or custom inductives for alternatives → catalog/T02-union-intersection.md
Generics (via type classes) — instance arguments [Ord α] serve as bounds → catalog/T04-generics-bounds.md
Derivation (limited) — deriving Repr, BEq, Inhabited; Mathlib extends further → catalog/T06-derivation.md
Extension methods (via scoped instances) — namespaced dot notation, open ... in → catalog/T19-extension-methods.md
Coherence (via scoping) — instance priority, scoped instance, overlap handling → catalog/T25-coherence-orphan.md
Self type (via dependent types) — no Self keyword; dependent types express this naturally → catalog/T33-self-type.md
Instance resolution — synthesis, backtracking, priority ordering → catalog/T37-trait-solver.md
Context functions (via instance arguments) — [Ord α] is automatically supplied → catalog/T42-context-functions.md
Associated types (via structure fields) — type-valued fields with outParam → catalog/T49-associated-types.md
Runtime polymorphism (via coercions + type classes) — heterogeneous collections, existential wrappers for open dispatch → catalog/T36-trait-objects.md
Functor / Applicative / Monad — native type classes; do-notation desugars to bind → catalog/T54-functor-applicative-monad.md
Monad transformers — StateT, ReaderT, ExceptT; MonadLift between layers → catalog/T55-monad-transformers.md
Tagless final (via type class abstraction) — polymorphic interpretation → catalog/T56-tagless-final.md
Typestate pattern — indexed inductive types for protocol states → catalog/T57-typestate.md
Witness & evidence types — Prop proofs as evidence; Decidable for runtime → catalog/T58-witness-evidence.md
Existential types — Sigma types, existential quantification → catalog/T59-existential-types.md
Recursive types — inductive types ARE recursive types; termination checked → catalog/T61-recursive-types.md
usecases/UC01-invalid-states.mdusecases/UC02-domain-modeling.mdusecases/UC03-exhaustiveness.mdusecases/UC12-compile-time.mdusecases/UC11-effect-tracking.mdusecases/UC04-generic-constraints.mdusecases/UC24-termination.mdusecases/UC10-encapsulation.mdnpx claudepluginhub jpablo/vibe-types --plugin vibe-typesAssists with Lean 4 theorem proving: editing .lean files, debugging builds (type mismatches, sorries, axioms, lake errors), searching mathlib lemmas, formalizing mathematics, and learning concepts via commands like /lean4:prove and /lean4:formalize.
Provides Lean 4 syntax guide for creating valid `--goal-type` and `--hypotheses` with `./bin/lc create-goal`. Covers function juxtaposition, real constants, set intervals, `;;`-separated hypotheses, and operators.
Explains Scala's advanced type system including generics, variance, type bounds, implicits, type classes, higher-kinded types, path-dependent types for type-safe APIs.