Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
2 changed files
with
9 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters