def Auto.Prep.elabLemma (stx : Lean.Term) (deriv : DTr) : Lean.Elab.Tactic.TacticM Lemma

From a user-provided term stx, produce a lemma

Equations

• One or more equations did not get rendered due to their size.

def Auto.Prep.addRecAsLemma (recVal : Lean.RecursorVal) : Lean.MetaM (Array Lemma)

Equations

• One or more equations did not get rendered due to their size.

def Auto.Prep.elabDefEq (name : Lean.Name) : Lean.Elab.Tactic.TacticM (Array Lemma)

Equations

• One or more equations did not get rendered due to their size.

def Auto.Prep.isNonemptyInhabited (ty : Lean.Expr) : Lean.MetaM Bool

Equations

• Auto.Prep.isNonemptyInhabited ty = do let __discr ← Lean.Meta.isClass? ty match __discr with | some name => pure (name == `Nonempty || name == `Inhabited) | x => pure false

structure Auto.Prep.ConstUnfoldInfo : Type

• name : Lean.Name
• val : Lean.Expr
• params : Array Lean.Name

def Auto.Prep.getConstUnfoldInfo (name : Lean.Name) : Lean.MetaM ConstUnfoldInfo

Equations

• One or more equations did not get rendered due to their size.

def Auto.Prep.topoSortUnfolds (unfolds : Array ConstUnfoldInfo) : Lean.MetaM (Array ConstUnfoldInfo)

Topologically sort constant names, such that the definition body of previous names does not use latter ones. If there is cyclic dependency, topoSortUnfolds throws an error

Equations

• One or more equations did not get rendered due to their size.

partial def Auto.Prep.topoSortUnfolds.go (depMap : Std.HashMap Lean.Name (Std.HashSet Lean.Name)) (stack : Std.HashSet Lean.Name) (n : Lean.Name) : StateRefT' IO.RealWorld (Std.HashSet Lean.Name × Array Lean.Name) Lean.MetaM Unit

def Auto.Prep.unfoldConsts (unfolds : Array ConstUnfoldInfo) (e : Lean.Expr) : Lean.Expr

Unfold constants occurring in expression e unfolds should satisfy the following constraint: ∀ i j, i < j → unfolds[j].name does not occur in unfolds[i].val

Equations

• One or more equations did not get rendered due to their size.