You can clone with
Added a journal entry.
Added a Suspension monad, which I will refactor into later.
Might as well just say vim instead of $EDITOR at this point.
Added a vim syntax file.
Implmented most of what we need to discharge by target language.
Implemented discharge by documentation.
Revert "Changed proposition syntax to the one I discussed in the jour…
This reverts commit f375de5.
Revert "Implemented leibniz substitution... but..."
This reverts commit 1ed3733.
Journaling -- deformalizing.
Implemented leibniz substitution... but...
Changed proposition syntax to the one I discussed in the journal.
Journaling about syntax for first-class propositions.
More journaling. Observe as my hopes are crushed.
Added another journal entry.
Don't erase error messages though.
Erase display before showing proof context.
Pretty printing contexts with HughesPJ combinators now.
Updated relation syntax from [(this) style] to ['this style] Still un…
…clear how to quantify over them.
Added two journal entries.
Fixed another code generation bug.
Fixed small bug in special character conversion.
Commented out the proof term in the generated code.
Renamed the floating document into a journal.
Added example of set modeling, moved design.mkd to doc, added some
brainstormy notes on higher-order logic.
Added undo, and observed some weird bug I couldn't reproduce. There was
a free variable in the goals...
Some error checking for intro tactic.
Intro tactic (no error checking)
Added Applicative Identity instance.
Fixed some bugs in program generation.
Code generation is broken, but at least extant. :-)