#explode
command #
Displays a proof term in a line by line format somewhat akin to a Fitch style proof or the Metamath proof style.
- reg : tactic.explode.status
- intro : tactic.explode.status
- lam : tactic.explode.status
- sintro : tactic.explode.status
Instances for tactic.explode.status
- tactic.explode.status.has_sizeof_inst
- tactic.explode.status.inhabited