sig fndef.


kind tm type.
kind ty type.
type truth, false       tm.
type neg, and, or, imp  tm.
type forall, some       tm.
type @ tm -> tm -> tm.            % application to a single argument
type abs string -> ty -> (tm -> tm) -> tm.       % abstraction
type form, term ty.
infixl @ 9.
%type fnmodule (list tm) -> tm.  % added by Liang
type copy tm -> tm -> o.
type const tm -> o.

kind def type.
type freevar string -> tm.   % intermediate abstract syntax for identifiers
type typesym string -> ty.  % type symbol


% for definitions:  
type tapp ty -> ty -> ty.   % type application abstract syntax.
type tm_coerce A -> tm.  % you know...
type ty_coerce A -> ty.


type zero		tm.
type succ		tm.	% successor
type nat		tm.	% natural number predicate
type var		tm -> o.	% variables

% typing
type arr		ty -> ty -> ty.	% arrow type
infixr arr 5.
type nt 		ty.	% naturals

type alldef		ty -> (tm -> def) -> def.	
type =^ 		tm -> tm -> def.		% definitional clause
infixl =^ 5.