An ott-like DSL embedded in Lean.
See the LottExamples directory for usage examples. Latex output is still a work in progress.
- Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and others. 2010. Ott: Effective tool support for the working semanticist. Journal of functional programming 20, 1 (2010), 71–122.
- Arthur Charguéraud. 2012. The locally nameless representation. Journal of automated reasoning 49, (2012), 363–408.