HLW: Code

In progress: a pandoc Haskell filter that parses code blocks with Lemmon-style proofs, transforms them to objects of type Proof, and then renders — either to html or latex.

To enter a Lemmon proof, just make a code block tagged with “lemmon”. It’s assumed that there is it least one whitespace between each column, but it’s not assumed that they are aligned (although that helps make the proof legible to humans).

```lemmon
1    (1) ¬P                       A
2    (2) Q                        A
1,2  (3) ¬P∧Q                     1,2 ∧I
4    (4) (¬P∧(Q∨R))→¬(S∧(¬T∨U))   A
```

Wish list

• Patch for emacs markdown mode that makes it easy to input Lemmon proofs
• Proof checker that operates on objects of type Proof
• Rendering to docx
• Define a Haskell data type for Fitch style proofs
• Transform between Lemmon and Fitch style proofs
• Collaborate with these guys carnap.io