Proof Checker
Load an example:
Examples:
Proof Input
Note: Press Esc + Tab to escape the proof input.
Output
Result
Settings
Enter your proof in the input box, below. As you type, the formatted proof will appear on the right, along with a validation status, beneath that. To learn the syntax, try playing with the examples, below, or see the language reference.
Note:x/g(c,d)
instead of
x/g(c, d)
!
= i
instead of
(Refl) and = e
instead of (Repl).
Load an example:
Examples:
Proof Input
Note: Press Esc + Tab to escape the proof input.
Output
Result
Settings