Lines Matching refs:function
42 (* This function divides up a list of applied constructors into a list
64 (* This function proves that constructors are distinct, ie, for each TY
121 (* the following function takes the constructor first in the list, (say
139 (* this function makes all the conjuncts for one type *)
222 We apply the appropriate distinctness function, getting
262 (* This function proves that constructors are one-to-one, ie, for each TY
353 extraction function will be called CON_arg.) *)
442 a pair consisting of the definition of the function and the name of
443 the function defined. *)
524 (* This function proves that for each value Vof type TY among the
622 (* the folowing function is nested so that