Lean4
/-- Debugging printer for proof objects. -/
def format : Proof → Std.Format
| .sorry => "sorry"
| .hyp i => Std.format i
| .triv => "triv"
| .exfalso' p => f! "(exfalso {p.format})"
| .intro x p => f! "(fun {x } ↦ {p.format})"
| .andLeft _ p => f! "{p.format} .1"
| .andRight _ p => f! "{p.format} .2"
| .andIntro _ p q => f! "⟨{p.format }, {q.format}⟩"
| .curry _ p => f! "(curry {p.format})"
| .curry₂ _ p q => f! "(curry {p.format } {q.format})"
| .app' p q => f! "({p.format } {q.format})"
| .orImpL p => f! "(orImpL {p.format})"
| .orImpR p => f! "(orImpR {p.format})"
| .orInL p => f! "(Or.inl {p.format})"
| .orInR p => f! "(Or.inr {p.format})"
| .orElim' p x q r => f! "({p.format }.elim (fun {x } ↦ {q.format }) (fun {x } ↦ {r.format})"
| .em false p => f! "(Decidable.em {p})"
| .em true p => f! "(Classical.em {p})"
| .decidableElim _ p x q r => f! "({p }.elim (fun {x } ↦ {q.format }) (fun {x } ↦ {r.format})"
| .impImpSimp _ p => f! "(impImpSimp {p.format})"
