Documentation
Lean
.
Meta
.
Injective
Search
Google site search
Lean
.
Meta
.
Injective
source
Imports
Init
Lean.Meta.Transform
Lean.Meta.Tactic.Apply
Lean.Meta.Tactic.Assumption
Lean.Meta.Tactic.Cases
Lean.Meta.Tactic.Injection
Lean.Meta.Tactic.Refl
Lean.Meta.Tactic.Subst
Lean.Meta.Tactic.Simp.Types
Imported by
Lean
.
Meta
.
elimOptParam
Lean
.
Meta
.
mkInjectiveTheoremNameFor
Lean
.
Meta
.
mkInjectiveEqTheoremNameFor
Lean
.
Meta
.
genInjectivity
Lean
.
Meta
.
mkInjectiveTheorems
source
def
Lean
.
Meta
.
elimOptParam
(type :
Lean.Expr
)
:
Lean.CoreM
Lean.Expr
Instances For
source
def
Lean
.
Meta
.
mkInjectiveTheoremNameFor
(ctorName :
Lake.Name
)
:
Lake.Name
Instances For
source
def
Lean
.
Meta
.
mkInjectiveEqTheoremNameFor
(ctorName :
Lake.Name
)
:
Lake.Name
Instances For
source
opaque
Lean
.
Meta
.
genInjectivity
:
Lean.Option
Bool
source
def
Lean
.
Meta
.
mkInjectiveTheorems
(declName :
Lake.Name
)
:
Lean.MetaM
Unit
Instances For