def TLA.ProofMode.tlaPmHyp : Lean.ParserDescr

Display syntax for a single proof-mode hypothesis.

Equations

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

def TLA.ProofMode.tlaPmEntails : Lean.ParserDescr

Display syntax for a proof-mode entailment.

Equations

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

def TLA.ProofMode.delabNameInNamedPred : Lean.PrettyPrinter.Delaborator.DelabM Lean.Ident

Delaborate the name component of a NamedPred.

Equations

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

def TLA.ProofMode.delabNamedPred : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax `TLA.ProofMode.tlaPmHyp)

Delaborate a NamedPred into a displayed hypothesis.

Equations

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

def TLA.ProofMode.delabNamedPredListAux (fuel : Nat) : Lean.PrettyPrinter.Delaborator.DelabM (List (Lean.TSyntax `TLA.ProofMode.tlaPmHyp))

Delaborate a List (NamedPred σ) expression into a list of proof-mode hypotheses. fuel bounds the list length and each recursive call drops one List.cons, so the expression's depth always suffices.

Equations

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

def TLA.ProofMode.delabNamedPredList : Lean.PrettyPrinter.Delaborator.DelabM (List (Lean.TSyntax `TLA.ProofMode.tlaPmHyp))

Delaborate a List (NamedPred σ) expression into a list of proof-mode hypotheses, seeding the fuel from the expression's approximate depth.

Equations

• TLA.ProofMode.delabNamedPredList = do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr TLA.ProofMode.delabNamedPredListAux (__do_lift.approxDepth.toNat + 1)

def TLA.ProofMode.delabEntails : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Entails goals, rendering them in proof-mode layout.

Equations

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