%
% '<cl>\doc\commands'
%

*** Section A: Starting CL ***

  cl path.cl           - import source module in `path.cl'
  cl path              - read from the binary module in `path.clb' if
                         it exists, otherwise do `cl path.cl'
  cl                   - the same as `cl default'

  The above commands import the specified modules into CL environment where the
modules can be viewed, modified.  Functions, predicates, and constants defined
in them can be also evaluated by means of a `query' .


*** Section B: Commands available in the CL environment ***

Commands when the cursor is large and not on a button:

  Alt x  Save the binary into `path.clb' and exit the CL system.

  Alt q  Execute the query given in the Query Command field.

  F3     Enter the modifiable (component or query) field. The query field can
         be also entered by any of the field modification commands (see
         Section C).

  Esc    Recompile all components which are marked by a `toothbrush',
         i.e. by a thin magenta line with downward pointing `bristles'.

Commands with the cursor on a button:

  Alt d  Delete a component below.

  Alt i  Insert a new component.

  F4:    If the button is for an include line then show the components of 
         the module specified by the include line. If the components are
         shown,  hide them by replacing the components with an include line.
         If the button is for a def-component show its internal form in the 
         result field. If the button is for a theorem show its (partial) 
         proof.

*** Section C: Environment Browsing and Editting commands ***

  F1     Shows the context sensitive description of the available editting
         commands in a help screen. This screen is exitted with Esc.

CL environment, as well as include, component, query and result fields can be
browsed by the following commands:

  Tab             Move to the query/result field.
  Left arrow      Move the cursor left.
  Right arrow     Move the cursor right.
  Up arrow        Move the cursor up.
  Down arrow      Move the cursor down.
  Home            Move the cursor to the begin of line.
  End             Move the curso to the end of line.
  PgUp            Move the cursor up the page.
  PgDn            Move the cursor down the page.
  Ctrl Home       Move the cursor to the begin of the environment/field.
  Ctrl End        Move the cursor to the end of the environment/field.
  Ctrl Pgup       Move to the top of the environment/field.
  Ctrl PgDn       Move to the bottom of the environment/field.

In the component and query fields the following field modification commands
can be given:

  Bksp            Delete the character before the cursor, join to the
                  previous line if at the begin of a line.
  Del             Delete the character under the cursor.
  Ctrl Bksp       Delete the current line.
  F5              Delete the current line.
  F6              Delete the characters from the cursor until the end of line.
  Enter           Split the line as indicated by the cursor.
  Ins             Toggle the insert/replace mode.
  Esc             Exit the field and trigger the compilation of a component
                  or a query. Exitting a component field disables the
                  subsequent components (this is shown by a `toothbrush').


*** Section D:  Syntax of CL ***

Module ::= mod Ident [ Includes ] [ Components ]
Includes ::= [ loc ] incl Ident [ , Path ] [ Includes ]
Components ::= { Remark | Definition | Theorem} [ Components ]
Remark ::= [ loc ] rem Text
Definition ::= [ loc ] [ free ] { fun | pred | const | prop } Ident [ Clauses ]
Theorem ::= [ loc ] thm Ident Form [ proof Proof ]

Clauses ::= Clause [ Clauses ]
Clause ::= Aform [ <- Aforms ]
Aforms ::= Aform [ & Aforms ]
Aform ::= [ ~ ] Application | Term Rel Term
Application ::= Ident(Term) | Ident Application
Term ::= Var [ : Ident ] | Num | Char | String | Term Op Term |
         Application [ Term ] | Term , Term | ( Term ) | "|" Term "|"
Form
Proof

Rel ::= = | != | < | <= | > | >= | in | !in

Op ::= + | - | * | / | mod | ++

   Priorities(decreasing): (* / mod) (+ - ++)
   Left associative:        * / mod   + - ++

Var
   Examples: i  x1  x99 zs  maximal_number_of_list

Ident
   Examples:  Fib  Maximal_number  N  Expr2string Born_1_jan_1997

Num
   Examples:  0  1  2   3   10   11  25  1997  123456789012345678901234567890

Char
   Examples:  "a"  "Z"  "1"  "+"  " "  "'"  """

String
   Note that the quote ' cannot occur in strings.

Text

Path