partial def mkEqTrans' (p₁ p₂ : Lean.Expr) : Lean.MetaM Lean.Expr

partial def mkHEqTrans' (p₁ p₂ : Lean.Expr) : Lean.MetaM Lean.Expr

partial def mkCongrArg' (f p : Lean.Expr) : Lean.MetaM Lean.Expr

def mkCongrFun' (h x : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

def mkCongr' (x₁ f₂ p1 p2 : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• mkCongr' x₁ f₂ p1 p2 = do let __do_lift ← mkCongrFun' p1 x₁ let __do_lift_1 ← mkCongrArg' f₂ p2 mkEqTrans' __do_lift __do_lift_1

def mkEqOfHEq' (h : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

def mkHEqOfEq' (h : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

@[irreducible]

def mkFunExt' (p : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• mkFunExt' p = do let y ← pure PUnit.unit (fun (y : PUnit) => Lean.Meta.mkFunExt p) y

partial def mkEqSymm' (h : Lean.Expr) : Lean.MetaM Lean.Expr

def mkPropExt' (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

partial def mkEqMPR' (e1 e2 : Lean.Expr) : Lean.MetaM Lean.Expr

def mkEqNDRec' (motive h1 h2 : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• mkEqNDRec' motive h1 h2 = do let __do_lift ← mkEqSymm' h2 let __do_lift ← Lean.Meta.mkCongrArg motive __do_lift mkEqMPR' __do_lift h1

partial def mkIteCongr1 (goal : Lean.MVarId) (p : Lean.Expr) : Lean.MetaM Unit

partial def mkIteCongr2 (goal : Lean.MVarId) (p : Lean.Expr) : Lean.MetaM Unit

partial def mkIteCongr3 (goal : Lean.MVarId) (p : Lean.Expr) : Lean.MetaM Unit

def mkIteCongr (goal p1 p2 p3 : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

partial def mkOfEqTrue' (p : Lean.Expr) : Lean.MetaM Lean.Expr

partial def simplify (e : Lean.Expr) : Lean.MetaM Lean.Expr

partial def getCalcProof (proof : Lean.Expr) : Lean.MetaM Lean.Term

partial def getCalcSteps (proof : Lean.Expr) (acc : Array (Lean.TSyntax `Lean.calcStep)) : Lean.MetaM (Array (Lean.TSyntax `Lean.calcStep))

def delabCalcProof (e : Lean.Expr) : Lean.MetaM (Lean.TSyntax `tactic)

Equations

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

def delabOfIffOfEqCalcProof (e : Lean.Expr) : Lean.MetaM (Lean.TSyntax `tactic)

Equations

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

def delabCalcTerm (e : Lean.Expr) : Lean.MetaM (Lean.TSyntax `term)

Equations

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

def delabMPRCalc (p1 p2 : Lean.Expr) : Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def delabOfEqTrueCalc (p : Lean.Expr) : Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def delabCalcSeq (p : Lean.Expr) : Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def delabTrivial (p : Lean.Expr) : Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def delabProof (e : Lean.Expr) : Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def calcifyTac : Lean.ParserDescr

Equations

• calcifyTac = Lean.ParserDescr.node `calcifyTac 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "calcify " false) (Lean.ParserDescr.const `tacticSeq))