lem
Tool merging math and logic for executable definitions
- Provided by: lem (Version: 2025-03-13+dfsg-1build1)
- Report a bug
DESCRIPTION
Lem 2025-03-13 example usage: lem -hol -ocaml test.lem
- -ocaml
- generate OCaml
- -tex
- generate LaTeX for each module separately
- -tex_all
- generate LaTeX in a single file
- -html
- generate Html
- -hol
- generate HOL
- -isa
- generate Isabelle
- -coq
- generate Coq
- -lem
- generate Lem output after simple transformations
- -ident
- generate input on stdout
- -lib
- add a library path, in addition to the standard library at '/build/lem-sZAePu/lem-2025-03-13+dfsg/debian/tmp/bin/library'. To change the latter, set the LEMLIB environment variable. Directories in the library path may optionally be associated with Isabelle session names, e.g. -lib MyLib=path/to/mylib. The standard library is associated with the session name LEM by default.
- -no_dep_reorder
- prohibit reordering modules given to lem as explicit arguments in order during dependency resolution
- -outdir
- the output directory (the default is the dir the files reside in)
- -i
- treat the file as input only and generate no output for it
- -only_changed_output
- generate only output files, whose content really changed compared to the existing file
- -only_auxiliary
- generate only auxiliary output files
- -auxiliary_level {none|auto|all}
- generate no (none) auxiliary-information, only auxiliaries that can be handled automatically (auto) or all (all) auxiliary information
- -debug
- print a backtrace for all errors (lem needs to be compiled in debug mode)
- -cerberus_pp
- special case HTML and LaTeX output for Cerberus Ail and Core
- -print_env
- print the environment signature on stdout
- -add_loc_annots
- add location annotations to the output
- -isa_path_imports
- use paths in Isabelle import statements instead of session-qualified imports
- -use_datatype_record
- use datatype_record instead of record in Isabelle output
- -v
- print version
- -ident_pat_compile
- activates pattern compilation for the identity backend. This is used for debugging.
- -ident_dict_passing
- activates dictionary passing transformations for the identity backend. This is used for debugging.
- -tex_suppress_target_names
- prints target-specific let-bindings as normal let bindings in the TeX backend.
- -tex_include_libraries
- include libraries in the TeX backend.
- -hol_remove_matches
- try to remove toplevel matches in HOL4 output.
- -prover_remove_failwith
- remove failwith branches in match statements in the prover backends.
- -suppress_renaming
- suppresses Lem's renaming facilities.
- -tex_all_force_library_output
- force library output with tex_all
- -report_default_instance_invocation
- reports the name of any default instance invoked at a given type.
-no_lifting_toplevel_match_for <type> Do not move cases over the given type to toplevel function case splits
- -wl {ign|warn|verb|err}
- warning level of all warnings
- -wl_gen {ign|warn|verb|err}
- warning level of miscellaneous warnings (default warn)
- -wl_amb_code {ign|warn|verb|err}
- warning level of ambiguous code (default warn)
- -wl_auto_import {ign|warn|verb|err}
- warning level of automatically imported modules (default ign)
- -wl_comp_message {ign|warn|verb|err}
- warning level of compile messages (default warn)
- -wl_inst_over {ign|warn|verb|err}
- warning level of overridden instance declarations (default ign)
- -wl_no_dec_eq {ign|warn|verb|err}
- warning level of equality of type is undecidable (default ign)
- -wl_pat_comp {ign|warn|verb|err}
- warning level of pattern compilation (default warn)
- -wl_pat_exh {ign|warn|verb|err}
- warning level of non-exhaustive pattern matches (default warn)
- -wl_pat_fail {ign|warn|verb|err}
- warning level of failed pattern compilation (default warn)
- -wl_pat_red {ign|warn|verb|err}
- warning level of redundant patterns (default warn)
- -wl_rename {ign|warn|verb|err}
- warning level of automatic renamings (default warn)
- -wl_resort {ign|warn|verb|err}
- warning level of resorted record fields and function clauses (default warn)
- -wl_unused_vars {ign|warn|verb|err}
- warning level of unused variables (default warn)
- -help
- Display this list of options
- --help
- Display this list of options
SEE ALSO
The full documentation for lem is maintained as a Texinfo manual. If the info and lem programs are properly installed at your site, the command
- info lem
should give you access to the complete manual.