package ott
A tool for writing definitions of programming languages and calculi
Install
Dune Dependency
Authors
Maintainers
Sources
0.30.tar.gz
sha256=ffd757e17d618a3162f0822e09b86d3879071e35378f47c9f6cdc16b757274ca
md5=bd83649b6ec5a4dbc22ed0de6a3a81f4
Description
Ott takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates output:
- a LaTeX source file that defines commands to build a typeset version of the definition;
- a Coq version of the definition;
- a HOL version of the definition;
- an Isabelle/HOL version of the definition;
- a Lem version of the definition;
- an OCaml version of the syntax of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by typeset terms.
Published: 25 Nov 2019
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page