Documentation
Lean
.
Elab
.
Tactic
.
Do
.
Syntax
Search
return to top
source
Imports
Init.NotationExtra
Lean.Elab.BuiltinNotation
Std.Do.PostCond
Std.Do.Triple.Basic
Imported by
Std
.
Do
.
Syntax
.
totalPostCond
source
def
Std
.
Do
.
Syntax
.
totalPostCond
:
Lean.Parser.Parser
Equations
One or more equations did not get rendered due to their size.
Instances For