wball/proof-checker
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

pretty printer now respects associativity

Browse source
This commit is contained in:
William Ball 2024-08-13 16:07:54 -07:00
parent 9cf96669e1
commit 55a1a9ce0a
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Formula.sml
View file

@ -122,10 +122,12 @@ struct
f ^ "(" ^ (String.concatWith ", " (map (Term.ppd d) args)) ^ ")" f ^ "(" ^ (String.concatWith ", " (map (Term.ppd d) args)) ^ ")"
| Equal (t, s) => Term.ppd d t ^ " = " ^ Term.ppd d s | Equal (t, s) => Term.ppd d t ^ " = " ^ Term.ppd d s
| Neg (Equal (t, s)) => Term.ppd d t ^ " != " ^ Term.ppd d s | Neg (Equal (t, s)) => Term.ppd d t ^ " != " ^ Term.ppd d s
| Neg phi => "~" ^ ppd d np phi | Neg phi => "\194\172" ^ ppd d np phi
| Conj (phi, psi) => ppd d np phi ^ " \226\136\167 " ^ ppd d np psi | Conj (phi, psi) =>
| Disj (phi, psi) => ppd d np phi ^ " \226\136\168 " ^ ppd d np psi ppd d np phi ^ " \226\136\167 " ^ ppd d (np + 1) psi
| Impl (phi, psi) => ppd d np phi ^ " => " ^ ppd d np psi | Disj (phi, psi) =>
ppd d np phi ^ " \226\136\168 " ^ ppd d (np + 1) psi
| Impl (phi, psi) => ppd d (np + 1) phi ^ " => " ^ ppd d np psi
| Iff (phi, psi) => ppd d np phi ^ " <=> " ^ ppd d np psi | Iff (phi, psi) => ppd d np phi ^ " <=> " ^ ppd d np psi
| Forall phi => "\226\136\128" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi | Forall phi => "\226\136\128" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi
| Exists phi => "\226\136\131" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi | Exists phi => "\226\136\131" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi