Description
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.
Published: 12 Dec 2022
Dependencies (6)
- num
-
zarith
>= "1.4"
-
conf-findutils
build
-
ocamlbuild
build
-
ocamlfind
build & >= "1.5.1"
-
ocaml
>= "4.07.0"
Reverse Dependencies (3)
Conflicts
-
None
Lem is a tool for lightweight executable mathematics
Install
copied = false, 2000)"
:class="{ 'border-gray-700': !copied, 'text-gray-100': !copied, 'focus:ring-orange-500': !copied, 'focus:border-orange-500': !copied, 'border-green-600': copied, 'text-green-600': copied, 'focus:ring-green-500': copied, 'focus:border-green-500': copied }">
Authors
Maintainers
Sources
2022-12-10.tar.gz
md5=d5e167df4aaefc3b64ef2dc28436130d
sha512=09b4fc9bdcd3ad95432bb8fbadef9025d3dece6a8d66c390eafc33d6c02ede5044d60291c2b46558905a5941df54a6f8cccf8be7865cbf028f4d9de3042f120e