NAME

       Ott - manual page for Ott version 0.34   distribution of Mon Dec 30 10:12:45 GMT 2024

DESCRIPTION

       Ott version 0.34   distribution of Mon Dec 30 10:12:45 GMT 2024

       usage: ott <options> <filename1> .. <filenamen>

       (use "OCAMLRUNPARAM=p
              ott ..." to show the ocamlyacc trace)

       (ott <options> <filename1> .. <filenamen>
              is equivalent to

              ott -i <filename1> .. -i <filenamen> <options>)

       -i <filename>
              Input file (can be used multiple times)

       -o <filename>
              Output file (can be used multiple times)

       -writesys <filename>
              Output system definition

       -readsys <filename>
              Input system definition

       -tex_filter <src><dst>
              Files to TeX filter

       -coq_filter <src><dst>
              Files to Coq filter

       -hol_filter <src><dst>
              Files to HOL filter

       -lem_filter <src><dst>
              Files to HOL filter

       -isa_filter <src><dst>
              Files to Isabelle filter

       -ocaml_filter <src><dst>
              Files to OCaml filter

       -merge <false>
              merge grammar and definition rules

       -parse <string>
              Test parse symterm,eg ":nontermroot: term"

       -fast_parse <false>
              do not parse :rulename: pseudoterminals

       -signal_parse_errors <false>
              return >0 if there are bad defns

       -picky_multiple_parses <false>
              Picky about multiple parses

       -quotient_rules <true>
              Quotient rules, as per {{ quotient-with ntr }} homs

       -generate_aux_rules <true>
              Generate auxiliary rules or constructor arguments from {{ aux ... }} homs

       -aux_style_rules <true>
              Auxiliary rules (true) vs constructor arguments (false)

       -output_source_locations <0>
              Include source location info in output (0=none, 1=drules, 2=grammar+drules)

       -colour <true>
              Use (vt220) colour for ASCII pretty print

       -show_sort <false>
              Show ASCII pretty print of syntax

       -show_defns <false>
              Show ASCII pretty print defns

       -tex_show_meta <true>
              Include meta prods and rules in TeX output

       -tex_show_categories <false>
              Signal production flags in TeX output

       -tex_suppress_category <[]>
              Suppress productions and rules with this category in TeX output

       -tex_suppress_ntr <[]>
              Suppress nonterminal root in TeX output

       -tex_colour <true>
              Colour parse errors in TeX output

       -tex_wrap <true>
              Wrap TeX output in document pre/postamble

       -tex_name_prefix <string>
              Prefix for tex commands (default "ott")

       -isabelle_primrec <true>
              Use "primrec" instead of "fun" for functions

       -isabelle_inductive <true>
              Use "inductive" instead of "inductive_set" for relations

       -isa_syntax <false>
              Use fancy syntax in Isabelle output

       -isa_generate_lemmas <false>
              Lemmas for collapsed functions in Isabelle

       -coq_avoid <1>
              coq type-name avoidance (0=nothing, 1=avoid, 2=secondaryify)

       -coq_expand_list_types <false>
              Expand list types in Coq output

       -coq_lngen <false>
              lngen compatibility

       -coq_names_in_rules <true>
              Copy user names in rule definitions

       -coq_use_filter_fn <false>
              Use list_filter instead of list_minus2 in substitutions

       -ocaml_include_terminals <false>
              Include terminals in OCaml output (experimental!)

       -ocaml_pp
              <target.ml  filename>  generate  OCaml  AST pretty printer files (experimental!) (also included in
              .mly target)

       -ocaml_pp_ast_module
              override default OCaml module name for AST module (experimental!)

       -ocaml_pp_json <false>
              Include JSON output in pretty printer (experimental)

       -pp_grammar
              (debug) print term grammar

       -dot <filename>
              (debug) dot graph of syntax dependencies

       -alltt <filename>
              (debug) alltt output of single source file

       -sort <true>
              (debug) do topological sort

       -process_defns <true>
              (debug) process inductive reln definitions

       -showraw <false>
              (debug) show raw grammar

       -ugly <false>
              (debug) use ugly ASCII output

       -no_rbcatn <true>
              (debug) remove relevant bind clauses

       -lem_debug
              (debug) print lem debug locations

       -help  Display this list of options

       --help Display this list of options

Ott version 0.34   distribution of Mon Dec 30 10... June 2025                                             OTT(1)