package lem

  1. Overview
  2. Docs

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: 06 Jun 2020

Dependencies (6)

  1. num
  2. zarith >= "1.4"
  3. conf-findutils build
  4. ocamlbuild build
  5. ocamlfind build & >= "1.5.1"
  6. ocaml >= "4.02.3" & < "5.0"

Dev Dependencies

None

Used by (3)

  1. libsail
  2. linksem
  3. sail < "0.15"

Conflicts

None