----------------------------------------------------------------------
Psyntax
----------------------------------------------------------------------
Psyntax : Psyntax_sig

SYNOPSIS
A structure that provides a tuple-style environment for term manipulation.

DESCRIBE
Each function in the {Psyntax} structure has a corresponding “record
version" in the {Rsyntax} structure, and vice versa. One can flip-flop
between the two structures by opening one and then the other. One can
also use long identifiers in order to use both syntaxes at once.

FAILURE
Never fails.

EXAMPLE
The following shows how to open the {Psyntax} structure and the
functions that subsequently become available in the top level
environment. Documentation for each of these functions is available
online.

   - open Psyntax;

This command results in the following functions entering the top-level
name-space.  Term creation functions:

   val mk_var = fn : string * hol_type -> term
   val mk_const = fn : string * hol_type -> term
   val mk_comb = fn : term * term -> term
   val mk_abs = fn : term * term -> term
   val mk_primed_var = fn : string * hol_type -> term
   val mk_eq = fn : term * term -> term
   val mk_imp = fn : term * term -> term
   val mk_select = fn : term * term -> term
   val mk_forall = fn : term * term -> term
   val mk_exists = fn : term * term -> term
   val mk_conj = fn : term * term -> term
   val mk_disj = fn : term * term -> term
   val mk_cond = fn : term * term * term -> term
   val mk_let = fn : term * term -> term

Term “destructor” functions (i.e., those functions that pull a term
apart, and reveal some of its internal structure):

   val dest_var = fn : term -> string * hol_type
   val dest_const = fn : term -> string * hol_type
   val dest_comb = fn : term -> term * term
   val dest_abs = fn : term -> term * term
   val dest_eq = fn : term -> term * term
   val dest_imp = fn : term -> term * term
   val dest_select = fn : term -> term * term
   val dest_forall = fn : term -> term * term
   val dest_exists = fn : term -> term * term
   val dest_conj = fn : term -> term * term
   val dest_disj = fn : term -> term * term
   val dest_cond = fn : term -> term * term * term
   val dest_let = fn : term -> term * term

The {lambda} datatype for taking terms apart, which is the range of the
{dest_term} function.

   datatype lambda =
      VAR of string * hol_type
    | CONST of {Name : string, Thy : string, Ty : hol_type}
    | COMB of term * term
    | LAMB of term * term
   val dest_term : term -> lambda


SEEALSO
Rsyntax.

----------------------------------------------------------------------