LEM(1)

NAME
lem - Tool merging math and logic for executable definitions

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-L0s441/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.