opaque lentil.pp.useDelab : Lean.Option Bool

Whether to use the custom TLA delaborator when pretty-printing.

opaque lentil.pp.autoRenderSatisfies : Lean.Option Bool

Whether to automatically render satisfies with the |=tla= notation.

def Parser.Attr.tla_nontemporal_def : Lean.ParserDescr

Marking the non-temporal parts of TLA.

Equations

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

def Parser.Attr.tla_nontemporal_def_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.tlasimp_def : Lean.ParserDescr

Marking the TLA definitions.

Equations

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

def Parser.Attr.tlasimp_def_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.execsimp_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.execsimp : Lean.ParserDescr

Marking the things to simplify when explicitly reasoning about exec.

Equations

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

def Parser.Attr.tla_finite_window_def : Lean.ParserDescr

Marking the definitions unfolded by tlaFiniteWindow.

Equations

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

def Parser.Attr.tla_finite_window_def_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.tlasimp_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.tlasimp : Lean.ParserDescr

Marking the theorems that can be simplify reasoning at the TLA level.

Equations

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

def Parser.Attr.tladual : Lean.ParserDescr

Marking the theorems that are dual to some existing theorems.

Equations

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

def Parser.Attr.tladual_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.tlanormsimp_proc : Lean.ParserDescr

Simplification procedure

Equations

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

def Parser.Attr.tlanormsimp : Lean.ParserDescr

Marking the theorems that are used for normalizing sequents.

Equations

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