sig fndefgram.
accum_sig lyaccshares,blists, fndef.

type fm tm -> gs.
type fe tm -> gs.	% terms
type te ty -> gs.	% types
type cl tm -> gs.	% clause  (could be type clause also!)
type dm, dl (list tm) -> gs.    % list of clauses
type lamt tm -> gs.     % lambda term
type pit, sigmat, slasht, andt, ort, impt, impbyt, negt, trutht, falset  gs.
type typet, arrowt, kindt gs.   % for types.
type definitiont, dott gs.
type fnmodt gs.
type idlst (list string) -> gs.
type fndefmod string -> (list tm) -> tm.  % abstract syntax for defs
type fnmodule string -> (list tm) -> tm.  % added by Liang
type formlam string -> tm -> tm -> o.
type  lparen  gs.
type  rparen  gs.
type  comma, tcomma  gs.
type  semicolon  gs.
type  dot  gs.
type tarrow  tm -> tm -> tm.


type typedef, kinddef (list string) -> ty -> tm. %intermdediate abstract syntax

type impby tm.   % intermediate syntax to distinguish definitions

% for natural numbers:

type zerot, natt, ntt, succt, formt   gs.
type telparen  gs.   % for making () grammar BRC(1,1).
type tep, kep  (list string) -> gs.

type tconst ty -> o.  		%type constants.
type tcopy ty -> ty -> o.  	%type substitution.

% for forming definitions: post-parsing operation
type is_capitalized string -> o.
type find_capitals tm -> (list string) -> o.
type makedef tm -> def -> o.
type form_def (list string) -> tm -> tm -> def -> o.
type fnparser o.