mbk/formal
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore: output tweaks

Browse source
This commit is contained in:
mehbark 2025-02-21 00:51:21 -05:00
parent 844933d57a
commit ed85f01850
1 changed files with 23 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
formal.scm
View file

@ -205,12 +205,13 @@
(return #f)))) (return #f))))
(proof-steps proof)) (proof-steps proof))
(when (or (member #f prems) (premises<=? goals prems)) (when (or (member #f prems) (premises<=? goals prems))
(printf "Proof complete!\n")
(return #t)) (return #t))
(format #t "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n" (printf "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
prems (filter (lambda (g) (not (member g prems))) goals))))) (reverse prems)
(filter (lambda (g) (not (member g prems))) goals)))))
;; TODO: i can just guess lol ;; TODO: this really isn't far from the macroless version....
;; this really isn't far from the macroless version....
(define and-comm (define and-comm
(proof (p q) (proof (p q)
(argument (p q) (argument (p q)
@ -228,3 +229,21 @@
[p simplification] [p simplification]
[q simplification] [q simplification]
[(pand q p) conjunction])) [(pand q p) conjunction]))
;; TODO: make this expressible better
;; TODO: use proofs for other proofs nicely
;; the mismatch between what is written and what is shown is hideous
;; avoidable by being explicit ig
(define and-assoc.inl
(proof (p q r)
(argument (p q r)
[(pand p (pand q r))]
[(pand (pand p q) r)])
[p simplification]
[(pand q r) simplification]
[q simplification]
[r simplification]
[(pand p q) conjunction]
[(pand (pand p q) r) conjunction]))
(proof-valid? and-assoc.inl)