sibylfs-lemversion

SibylFS fork of Lightweight Executable Mathematics for large-scale semantics

Lem is a tool for lightweight executable mathematics, for writing, managing, and publishing large-scale portable semantic definitions, with export to LaTeX, executable code (currently OCaml) and interactive theorem provers (currently Coq, HOL4, and Isabelle/HOL).

It is also intended as an intermediate language for generating definitions from domain-specific tools, and for porting definitions between interactive theorem proving systems.

Lem is under active development and has been used in several applications, some of which can be found in the examples directory. It is made available under the BSD 3-clause license, with the exception of a few files derived from OCaml, which are under the GNU Library GPL.

AuthorThe Lem Team
Published
Homepagehttps://bitbucket.org/Peter_Sewell/lem
Maintainertom.j.ridge@googlemail.com
Dependencies
Optional dependencies
Conflicts
Source [http] https://github.com/ocaml/opam-source-archives/raw/main/sibylfs-lem-0.4.0.tar.gz
md5=9306b3bdc99638d5895156c840033b86
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/sibylfs-lem/sibylfs-lem.0.4.0/opam
Required by