lott

An ott-like DSL embedded in Lean.

See the LottExamples directory for usage examples. Latex output is still a work in progress.

References

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.

Name		Name	Last commit message	Last commit date
Latest commit History 41 Commits
.github/workflows		.github/workflows
Lott		Lott
LottExamples		LottExamples
nix		nix
.envrc		.envrc
.gitignore		.gitignore
Lott.lean		Lott.lean
LottExamples.lean		LottExamples.lean
README.md		README.md
lake-manifest.json		lake-manifest.json
lakefile.lean		lakefile.lean
lean-toolchain		lean-toolchain