def LentilLib.simpleAddTheorem (name : Lean.Name) (lvlParams : List Lean.Name) (type value : Lean.Expr) (nonComputable? : Bool) : Lean.CoreM Unit

Add a single theorem to the environment by providing its name, type and proof.

Equations

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

def LentilLib.simpleProveTheorem (name : Lean.Name) (lvlParams : List Lean.Name) (type : Lean.Expr) (proofScript : Lean.TSyntax `term) (nonComputable? : Bool) : Lean.MetaM Unit

Prove a theorem at the level of MetaM, without going into the proof mode.

Equations

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

def LentilLib.mkUnusedName (names : List Lean.Name) (baseName : Lean.Name) : Lean.Name

Gives a name based on baseName that's not already in the list.

Equations

• LentilLib.mkUnusedName names baseName = if (!names.contains baseName) = true then baseName else LentilLib.mkUnusedNameLoop✝ names baseName 1 (names.length + 1)

def LentilLib.termIdentOpt (stx : Lean.TSyntax `term) : Lean.Elab.Tactic.TacticM (Option (Lean.TSyntax `ident))

Is stx, a Term, an Ident?

Equations

• LentilLib.termIdentOpt stx = bif false || stx.raw.isOfKind `ident then have id := { raw := stx.raw }; pure (some id) else have __discr := stx; pure none

def LentilLib.let (g : Lean.MVarId) (h : Lean.Name) (v : Lean.Expr) (t : Option Lean.Expr := none) : Lean.MetaM (Lean.FVarId × Lean.MVarId)

Add the hypothesis h : t, given v : t, and return the new FVarId.

Equations

• LentilLib.let g h v t = do let __do_lift ← t.getDM (Lean.Meta.inferType v) let __do_lift ← g.define h __do_lift v __do_lift.intro1P