---
name: "lem"
section: "1"
platform: "linux"
package: "lem"
version: "2022-12-10+dfsg2-4+b2"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/lem"
---

# lem(1)

Tool merging math and logic for executable definitions

## 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/reproducible-path/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.