HLF

HLF is an implementation of LF ala Twelf. It is implemented as a DSL within Haskell because I hate parsing.

For some examples of how to actually use this look at examples/. Notably this includes the code for the typing judgments of simply typed lambda calculus and natural number examples.

For building, all you need to do is the usual

cabal sandbox init
cabal install # Watch 50% of hackage install with lens

And then you can tinker around with toy examples.