package ott
Ott is a tool for writing definitions of programming languages and calculi
Install
Dune Dependency
Authors
Maintainers
Sources
0.27.tar.gz
sha256=e0ebb3742a6632312cf4de71dad4e4eadfe420b6b86a5d6df6776c4135044ac5
md5=e05eea1b975d8612c68feec068c4b963
Description
It 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 LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by target-system terms.
Published: 29 Nov 2017
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page