ReferenceManual

• Ctrl-D
• ! <command>
• #define <pattern> := <term> .
• **, **>
• --, -->
• .
• =
• =(n)=>, =(n,m)=>, =()=>
• =*=
• =/=
• ==
• ==>
• ? [<term>]
• ?apropos <term> [<term> ...]
• ?com [ <term> ]
• [
• accept =*= proof switch
• all axioms switch
• always memo switch
• :apply (<tactic> ...) [to <goal-name>]
• apply <action> [ <subst> ] <range> <selection>
• :auto
• auto context switch
• autoload <module-name> <file-name>
• ax [ <label-exp> ] <term> = <term> .
• axioms { <decls> }
• :backward equation|rule
• bax [ <label-exp> ] <term> = <term> .
• bceq [ <label-exp> ] <term> = <term> if <boolterm> .
• bcrule [ <label-exp> ] <term> => <term> if <term> .
• bctrans [ <label-exp> ] <term> => <term> if <bool> .
• beq [ <label-exp> ] <term> = <term> .
• bgoal <term> .
• {bguess | :bguess} {imply|and|or} [ with <predicate name> ]
• binspect [in <module-name> :] <boolean-term> .
• :binspect [in <goal-name> :] <boolean-term> .
• bop <op-spec> : <sorts> -> <sort>
• bpred <op-spec> : <sorts>
• breduce [ in <mod-exp> : ] <term> .
• {bresolve | :bresolve} [<limit>] [all]
• brule [ <label-exp> ] <term> => <term> .
• {bshow | :bshow} [{ tree | grind }]
• bsort token-predicate creater printer term-predicate
• btrans [ <label-exp> ] <term> => <term> .
• cbred [ in <mod-exp> :] <term> .
• cd <dirname>
• ceq [ <label-exp> ] <term> = <term> if <boolterm> .
• check <options>
• check <something> switch
• choose <selection>
• CITP
• clause <term> .
• clean memo
• clean memo switch
• close
• commands
• comments
• cond limit switch
• cont
• :cp { "[" <label> "]" | "(" <sentence> . ")" } >< { "[" <label> "]" | "(" <sentence> .")" }
• crule [ <label-exp> ] <term> => <term> if <term> .
• :csp { eq [ <label-exp>] <term> = <term> . ...}
• :csp- { eq [ <label-exp>] <term> = <term> . ...}
• :ctf { eq [ <label-exp> ] <term> = <term> .}
• :ctf- { eq [ <label-exp> ] <term> = <term> .}
• ctrans [ <label-exp> ] <term> => <term> if <term> .
• db reset
• :def <symbol> = { <ctf> | <csp> | <init> }
• demod
• :describe proof
• describe <something>
• dirs
• dribble { <file-name> | .}
• :embed (<label> ... <label>) as <module_name>
• eof
• eq [ <label-exp> ] <term> = <term> .
• :equation
• esc return
• exec limit switch
• exec trace switch
• exec! [ in <mod-exp> : ] <term> .
• execute [ in <mod-exp> : ] <term> .
• extending ( <modexp> )
• find {+rule | -rule}
• find all rules switch
• flag(<name>, { on | off })
• full reset
• gendoc <pathname>
• :goal { <sentence> . ... }
• goal <term> .
• :imp "[" <label> "]" by "{" <variable> <- <term>; ..."}"
• imports { <import-decl> }
• include BOOL switch
• include RWL switch
• including ( <modexp> )
• init [as <name>] { "[" <label> "]" | "(" <sentence> "")} by "{" <variable> <- <term>; ... "}"
• :init [as <name>] { "[" <label> "]" | "(" <sentence> "")} by "{" <variable> <- <term>; ... "}"
• input <pathname>
• inspect <term>
• instantiation of parameterized modules
• :is
• let <identifier> = <term> .
• lex (<op>, ..., <op>)
• libpath switch
• lisp
• lispq
• list { axiom | sos | usable | flag | param | option | demod }
• look up <something>
• ls <pathname>
• make <mod_name> ( <mod_exp> )
• match <term_spec> to <pattern> .
• memo switch
• [sys:]module[!|*] <modname> [ ( <params> ) ] [ <principal_sort_spec> ] { mod_elements ... }
• module expression
• names <mod-exp> .
• no autoload <module-name>
• :normalize { on | off}
• on-the-fly declarations
• op <op-spec> : <sorts> -> <sort> { <attribute-list> }
• open <mod_exp> .
• operator attributes
• operator precedence
• option { reset | = <name> }
• :order (<op>, ..., <op>)
• param(<name>, <value>)
• parameterized module
• parse [ in <mod-exp> : ] <term> .
• parse normalize switch
• popd
• pred <op-spec> : <sorts>
• prelude <file>
• print depth switch
• print mode switch
• print trs switch
• protect <module-name>
• protecting ( <modexp> )
• provide <feature>
• pushd <directory>
• pvar <var-name> : <sort-name>
• pwd
• qualified sort/operator/parameter
• qualified term
• quiet switch
• quit
• { :red | :exec | :bred } [in <goal-name> :] <term> .
• reduce [ in <mod-exp> : ] <term> .
• reduce conditions switch
• regularize <mod-name>
• regularize signature switch
• require <feature> [ <pathname> ]
• :reset
• reset
• resolve {. | <file-path> }
• restore <pathname>
• rewrite limit switch
• :roll back
• :rule
• rule [ <label-exp> ] <term> => <term> .
• save <pathname>
• save-option <name>
• scase (<term>) in (<mod-exp>) as <name> { <decl> ..} : <term> .
• search predicates
• :select <goal-name>
• select <mod_exp> .
• :set(<name>, { on | off | show })
• set <name> [option] <value>
• :show goal|unproved|proof|discharged
• show <something>
• show mode switch
• sigmatch (<mod-exp>) to (<mod-exp>)
• signature { <sig-decl> }
• sort declaration
• sos { = | + | - } { <clause> , ... }
• :spoiler { on | off}
• start <term> .
• statistics switch
• step switch
• stop
• stop pattern switch
• switches
• :theory <op_name> : <arity> -> <coarity> { assoc | comm | id: <term> }
• trace [whole] switch
• trans [ <label-exp> ] <term> => <term> .
• unprotect <module-name>
• :use (<label> ... <label>)
• using ( <modexp> )
• var <var-name> : <sort-name>
• :verbose { on | off }
• verbose switch
• version
• view <name> from <modname> to <modname> { <viewelems> }