3 ms·
Most of the things I want to do end up meaning that I need a logical framework in which to build a type theory. I use Agda for that, but this is not its strengt
by jonsterling 13y ago
Most of the things I want to do end up meaning that I need a logical framework in which to build a type theory. I use Agda for that, but this is not its strength (try building a non-trivial term language with binding, for instance).
- tel 12y agoI never realized it could be much easier than Agda, but I've been playing with Twelf now for a little bit and am getting a feel for how LF and HOAS work together.