NAME

       lem - Tool merging math and logic for executable definitions

DESCRIPTION

       Lem 2022-12-10 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-nSgrhc/lem-2022-12-10+dfsg2/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.

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