Opam Package lem.2020-06-03

Package info

opam-namelem
opam-version2020-06-03
synopsisLem is a tool for lightweight executable mathematics
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.
authors
  • Dominic Mulligan
  • Francesco Zappa Nardelli
  • Gabriel Kerneis
  • Kathy Gray
  • Peter Boehm
  • Peter Sewell
  • Scott Owens
  • Thomas Tuerk
  • Brian Campbell
  • Shaked Flur
  • Thomas Bauereiss
  • Stephen Kell
  • Thomas Williams
  • Lars Hupel
  • Basile Clement
homepagehttp://www.cl.cam.ac.uk/~pes20/lem/
licensepart BSD3, part LGPL 2
deps (6)
revdeps (2)
metas (3)
libraries (1)

Package modules

Package sources

lem

Package files

share/lem/library/word.lem
share/lem/library/tuple.lem
share/lem/library/transform.lem
share/lem/library/string_extra.lem
share/lem/library/string.lem
share/lem/library/sorting.lem
share/lem/library/show_extra.lem
share/lem/library/show.lem
share/lem/library/set_helpers.lem
share/lem/library/set_extra.lem
share/lem/library/set.lem
share/lem/library/relation.lem
share/lem/library/pervasives_extra.lem
share/lem/library/pervasives.lem
share/lem/library/ocaml_constants
share/lem/library/num_extra.lem
share/lem/library/num.lem
share/lem/library/maybe_extra.lem
share/lem/library/maybe.lem
share/lem/library/map_extra.lem
share/lem/library/map.lem
share/lem/library/machine_word.lem
share/lem/library/list_extra.lem
share/lem/library/list.lem
share/lem/library/isabelle_constants
share/lem/library/hol_constants
share/lem/library/function_extra.lem
share/lem/library/function.lem
share/lem/library/either.lem
share/lem/library/debug.lem
share/lem/library/coq_constants
share/lem/library/bool.lem
share/lem/library/basic_classes.lem
share/lem/library/assert_extra.lem
share/lem/library
share/lem/isabelle-lib/ROOT
share/lem/isabelle-lib/Lem_word.thy
share/lem/isabelle-lib/Lem_tuple.thy
share/lem/isabelle-lib/Lem_string_extra.thy
share/lem/isabelle-lib/Lem_string.thy
share/lem/isabelle-lib/Lem_sorting.thy
share/lem/isabelle-lib/Lem_show_extra.thy
share/lem/isabelle-lib/Lem_show.thy
share/lem/isabelle-lib/Lem_set_helpers.thy
share/lem/isabelle-lib/Lem_set_extra.thy
share/lem/isabelle-lib/Lem_set.thy
share/lem/isabelle-lib/Lem_relation.thy
share/lem/isabelle-lib/Lem_pervasives_extra.thy
share/lem/isabelle-lib/Lem_pervasives.thy
share/lem/isabelle-lib/Lem_num_extra.thy
share/lem/isabelle-lib/Lem_num.thy
share/lem/isabelle-lib/Lem_maybe_extra.thy
share/lem/isabelle-lib/Lem_maybe.thy
share/lem/isabelle-lib/Lem_map_extra.thy
share/lem/isabelle-lib/Lem_map.thy
share/lem/isabelle-lib/Lem_machine_word.thy
share/lem/isabelle-lib/Lem_list_extra.thy
share/lem/isabelle-lib/Lem_list.thy
share/lem/isabelle-lib/Lem_function_extra.thy
share/lem/isabelle-lib/Lem_function.thy
share/lem/isabelle-lib/Lem_either.thy
share/lem/isabelle-lib/Lem_bool.thy
share/lem/isabelle-lib/Lem_basic_classes.thy
share/lem/isabelle-lib/Lem_assert_extra.thy
share/lem/isabelle-lib/LemExtraDefs.thy
share/lem/isabelle-lib/Lem.thy
share/lem/isabelle-lib
share/lem/hol-lib/lem_wordScript.sml
share/lem/hol-lib/lem_tupleScript.sml
share/lem/hol-lib/lem_string_extraScript.sml
share/lem/hol-lib/lem_stringScript.sml
share/lem/hol-lib/lem_sortingScript.sml
share/lem/hol-lib/lem_show_extraScript.sml
share/lem/hol-lib/lem_showScript.sml
share/lem/hol-lib/lem_set_helpersScript.sml
share/lem/hol-lib/lem_set_extraScript.sml
share/lem/hol-lib/lem_setScript.sml
share/lem/hol-lib/lem_relationScript.sml
share/lem/hol-lib/lem_pervasives_extraScript.sml
share/lem/hol-lib/lem_pervasivesScript.sml
share/lem/hol-lib/lem_num_extraScript.sml
share/lem/hol-lib/lem_numScript.sml
share/lem/hol-lib/lem_maybe_extraScript.sml
share/lem/hol-lib/lem_maybeScript.sml
share/lem/hol-lib/lem_map_extraScript.sml
share/lem/hol-lib/lem_mapScript.sml
share/lem/hol-lib/lem_machine_wordScript.sml
share/lem/hol-lib/lem_list_extraScript.sml
share/lem/hol-lib/lem_listScript.sml
share/lem/hol-lib/lem_function_extraScript.sml
share/lem/hol-lib/lem_functionScript.sml
share/lem/hol-lib/lem_eitherScript.sml
share/lem/hol-lib/lem_boolScript.sml
share/lem/hol-lib/lem_basic_classesScript.sml
share/lem/hol-lib/lem_assert_extraScript.sml
share/lem/hol-lib/lemScript.sml
share/lem/hol-lib/lemLib.sml
share/lem/hol-lib/Holmakefile
share/lem/hol-lib
share/lem/coq-lib/lem_word_auxiliary.v
share/lem/coq-lib/lem_word.v
share/lem/coq-lib/lem_tuple_auxiliary.v
share/lem/coq-lib/lem_tuple.v
share/lem/coq-lib/lem_string_extra_auxiliary.v
share/lem/coq-lib/lem_string_extra.v
share/lem/coq-lib/lem_string_auxiliary.v
share/lem/coq-lib/lem_string.v
share/lem/coq-lib/lem_sorting_auxiliary.v
share/lem/coq-lib/lem_sorting.v
share/lem/coq-lib/lem_show_extra_auxiliary.v
share/lem/coq-lib/lem_show_extra.v
share/lem/coq-lib/lem_show_auxiliary.v
share/lem/coq-lib/lem_show.v
share/lem/coq-lib/lem_set_helpers_auxiliary.v
share/lem/coq-lib/lem_set_helpers.v
share/lem/coq-lib/lem_set_extra_auxiliary.v
share/lem/coq-lib/lem_set_extra.v
share/lem/coq-lib/lem_set_auxiliary.v
share/lem/coq-lib/lem_set.v
share/lem/coq-lib/lem_relation_auxiliary.v
share/lem/coq-lib/lem_relation.v
share/lem/coq-lib/lem_pervasives_extra_auxiliary.v
share/lem/coq-lib/lem_pervasives_extra.v
share/lem/coq-lib/lem_pervasives_auxiliary.v
share/lem/coq-lib/lem_pervasives.v
share/lem/coq-lib/lem_num_extra_auxiliary.v
share/lem/coq-lib/lem_num_extra.v
share/lem/coq-lib/lem_num_auxiliary.v
share/lem/coq-lib/lem_num.v
share/lem/coq-lib/lem_maybe_extra_auxiliary.v
share/lem/coq-lib/lem_maybe_extra.v
share/lem/coq-lib/lem_maybe_auxiliary.v
share/lem/coq-lib/lem_maybe.v
share/lem/coq-lib/lem_map_extra_auxiliary.v
share/lem/coq-lib/lem_map_extra.v
share/lem/coq-lib/lem_map_auxiliary.v
share/lem/coq-lib/lem_map.v
share/lem/coq-lib/lem_machine_word_auxiliary.v
share/lem/coq-lib/lem_machine_word.v
share/lem/coq-lib/lem_list_extra_auxiliary.v
share/lem/coq-lib/lem_list_extra.v
share/lem/coq-lib/lem_list_auxiliary.v
share/lem/coq-lib/lem_list.v
share/lem/coq-lib/lem_function_extra_auxiliary.v
share/lem/coq-lib/lem_function_extra.v
share/lem/coq-lib/lem_function_auxiliary.v
share/lem/coq-lib/lem_function.v
share/lem/coq-lib/lem_either_auxiliary.v
share/lem/coq-lib/lem_either.v
share/lem/coq-lib/lem_bool_auxiliary.v
share/lem/coq-lib/lem_bool.v
share/lem/coq-lib/lem_basic_classes_auxiliary.v
share/lem/coq-lib/lem_basic_classes.v
share/lem/coq-lib/lem_assert_extra_auxiliary.v
share/lem/coq-lib/lem_assert_extra.v
share/lem/coq-lib/coqharness.v
share/lem/coq-lib/coq_makefile.in
share/lem/coq-lib
share/lem
lib/lem_zarith/xstring.mli
lib/lem_zarith/xstring.cmx
lib/lem_zarith/xstring.cmi
lib/lem_zarith/vector.mli
lib/lem_zarith/vector.cmx
lib/lem_zarith/vector.cmi
lib/lem_zarith/rational_impl.mli
lib/lem_zarith/rational_impl.cmx
lib/lem_zarith/rational_impl.cmi
lib/lem_zarith/rational.mli
lib/lem_zarith/rational.cmx
lib/lem_zarith/rational.cmi
lib/lem_zarith/pset.mli
lib/lem_zarith/pset.cmx
lib/lem_zarith/pset.cmi
lib/lem_zarith/pmap.mli
lib/lem_zarith/pmap.cmx
lib/lem_zarith/pmap.cmi
lib/lem_zarith/nat_num.mli
lib/lem_zarith/nat_num.cmx
lib/lem_zarith/nat_num.cmi
lib/lem_zarith/nat_big_num.mli
lib/lem_zarith/nat_big_num.cmx
lib/lem_zarith/nat_big_num.cmi
lib/lem_zarith/lem_word.cmx
lib/lem_zarith/lem_word.cmi
lib/lem_zarith/lem_tuple.cmx
lib/lem_zarith/lem_tuple.cmi
lib/lem_zarith/lem_string_extra.cmx
lib/lem_zarith/lem_string_extra.cmi
lib/lem_zarith/lem_string.cmx
lib/lem_zarith/lem_string.cmi
lib/lem_zarith/lem_sorting.cmx
lib/lem_zarith/lem_sorting.cmi
lib/lem_zarith/lem_show_extra.cmx
lib/lem_zarith/lem_show_extra.cmi
lib/lem_zarith/lem_show.cmx
lib/lem_zarith/lem_show.cmi
lib/lem_zarith/lem_set_helpers.cmx
lib/lem_zarith/lem_set_helpers.cmi
lib/lem_zarith/lem_set_extra.cmx
lib/lem_zarith/lem_set_extra.cmi
lib/lem_zarith/lem_set.cmx
lib/lem_zarith/lem_set.cmi
lib/lem_zarith/lem_relation.cmx
lib/lem_zarith/lem_relation.cmi
lib/lem_zarith/lem_pervasives_extra.cmx
lib/lem_zarith/lem_pervasives_extra.cmi
lib/lem_zarith/lem_pervasives.cmx
lib/lem_zarith/lem_pervasives.cmi
lib/lem_zarith/lem_num_extra.cmx
lib/lem_zarith/lem_num_extra.cmi
lib/lem_zarith/lem_num.cmx
lib/lem_zarith/lem_num.cmi
lib/lem_zarith/lem_maybe_extra.cmx
lib/lem_zarith/lem_maybe_extra.cmi
lib/lem_zarith/lem_maybe.cmx
lib/lem_zarith/lem_maybe.cmi
lib/lem_zarith/lem_map_extra.cmx
lib/lem_zarith/lem_map_extra.cmi
lib/lem_zarith/lem_map.cmx
lib/lem_zarith/lem_map.cmi
lib/lem_zarith/lem_machine_word.cmx
lib/lem_zarith/lem_machine_word.cmi
lib/lem_zarith/lem_list_extra.cmx
lib/lem_zarith/lem_list_extra.cmi
lib/lem_zarith/lem_list.cmx
lib/lem_zarith/lem_list.cmi
lib/lem_zarith/lem_function_extra.cmx
lib/lem_zarith/lem_function_extra.cmi
lib/lem_zarith/lem_function.cmx
lib/lem_zarith/lem_function.cmi
lib/lem_zarith/lem_either.cmx
lib/lem_zarith/lem_either.cmi
lib/lem_zarith/lem_bool.cmx
lib/lem_zarith/lem_bool.cmi
lib/lem_zarith/lem_basic_classes.cmx
lib/lem_zarith/lem_basic_classes.cmi
lib/lem_zarith/lem_assert_extra.cmx
lib/lem_zarith/lem_assert_extra.cmi
lib/lem_zarith/lem.cmx
lib/lem_zarith/lem.cmi
lib/lem_zarith/extract.cmxa
lib/lem_zarith/extract.cma
lib/lem_zarith/extract.a
lib/lem_zarith/either.cmx
lib/lem_zarith/either.cmi
lib/lem_zarith/bit.mli
lib/lem_zarith/bit.cmx
lib/lem_zarith/bit.cmi
lib/lem_zarith/big_int_impl.mli
lib/lem_zarith/big_int_impl.cmx
lib/lem_zarith/big_int_impl.cmi
lib/lem_zarith/META
lib/lem_zarith
lib/lem_num/xstring.mli
lib/lem_num/xstring.cmx
lib/lem_num/xstring.cmi
lib/lem_num/vector.mli
lib/lem_num/vector.cmx
lib/lem_num/vector.cmi
lib/lem_num/rational_impl.mli
lib/lem_num/rational_impl.cmx
lib/lem_num/rational_impl.cmi
lib/lem_num/rational.mli
lib/lem_num/rational.cmx
lib/lem_num/rational.cmi
lib/lem_num/pset.mli
lib/lem_num/pset.cmx
lib/lem_num/pset.cmi
lib/lem_num/pmap.mli
lib/lem_num/pmap.cmx
lib/lem_num/pmap.cmi
lib/lem_num/nat_num.mli
lib/lem_num/nat_num.cmx
lib/lem_num/nat_num.cmi
lib/lem_num/nat_big_num.mli
lib/lem_num/nat_big_num.cmx
lib/lem_num/nat_big_num.cmi
lib/lem_num/lem_word.cmx
lib/lem_num/lem_word.cmi
lib/lem_num/lem_tuple.cmx
lib/lem_num/lem_tuple.cmi
lib/lem_num/lem_string_extra.cmx
lib/lem_num/lem_string_extra.cmi
lib/lem_num/lem_string.cmx
lib/lem_num/lem_string.cmi
lib/lem_num/lem_sorting.cmx
lib/lem_num/lem_sorting.cmi
lib/lem_num/lem_show_extra.cmx
lib/lem_num/lem_show_extra.cmi
lib/lem_num/lem_show.cmx
lib/lem_num/lem_show.cmi
lib/lem_num/lem_set_helpers.cmx
lib/lem_num/lem_set_helpers.cmi
lib/lem_num/lem_set_extra.cmx
lib/lem_num/lem_set_extra.cmi
lib/lem_num/lem_set.cmx
lib/lem_num/lem_set.cmi
lib/lem_num/lem_relation.cmx
lib/lem_num/lem_relation.cmi
lib/lem_num/lem_pervasives_extra.cmx
lib/lem_num/lem_pervasives_extra.cmi
lib/lem_num/lem_pervasives.cmx
lib/lem_num/lem_pervasives.cmi
lib/lem_num/lem_num_extra.cmx
lib/lem_num/lem_num_extra.cmi
lib/lem_num/lem_num.cmx
lib/lem_num/lem_num.cmi
lib/lem_num/lem_maybe_extra.cmx
lib/lem_num/lem_maybe_extra.cmi
lib/lem_num/lem_maybe.cmx
lib/lem_num/lem_maybe.cmi
lib/lem_num/lem_map_extra.cmx
lib/lem_num/lem_map_extra.cmi
lib/lem_num/lem_map.cmx
lib/lem_num/lem_map.cmi
lib/lem_num/lem_machine_word.cmx
lib/lem_num/lem_machine_word.cmi
lib/lem_num/lem_list_extra.cmx
lib/lem_num/lem_list_extra.cmi
lib/lem_num/lem_list.cmx
lib/lem_num/lem_list.cmi
lib/lem_num/lem_function_extra.cmx
lib/lem_num/lem_function_extra.cmi
lib/lem_num/lem_function.cmx
lib/lem_num/lem_function.cmi
lib/lem_num/lem_either.cmx
lib/lem_num/lem_either.cmi
lib/lem_num/lem_bool.cmx
lib/lem_num/lem_bool.cmi
lib/lem_num/lem_basic_classes.cmx
lib/lem_num/lem_basic_classes.cmi
lib/lem_num/lem_assert_extra.cmx
lib/lem_num/lem_assert_extra.cmi
lib/lem_num/lem.cmx
lib/lem_num/lem.cmi
lib/lem_num/extract.cmxa
lib/lem_num/extract.cma
lib/lem_num/extract.a
lib/lem_num/either.cmx
lib/lem_num/either.cmi
lib/lem_num/bit.mli
lib/lem_num/bit.cmx
lib/lem_num/bit.cmi
lib/lem_num/big_int_impl.mli
lib/lem_num/big_int_impl.cmx
lib/lem_num/big_int_impl.cmi
lib/lem_num/META
lib/lem_num
lib/lem/META
lib/lem
bin/lem