©1998 Research Institute for Symbolic Computation (RISC-Linz)
This package contains the implementation of the type checker used by the CFLP calculus. The type checker is based on the Hindley--Milner type system.
Syntax call
NewTyVar[ ]
Output
a fresh type variable
Implementation
Syntax call
Tc[ term ]
Input
term : a term
Output
the type of term if term is well typed
"⊥" otherwise
Implementation
Syntax call
TcX[ term, &tgr; , type--eqs, type--vars ]
Input
Output
a pair {type--eqs', type--vars'} where
Implementation
Syntax call
TcXList[{ term1, term2, ... }, { type1, type2, ... }, type--eqs, type--vars ]
Input
Output
a pair {type--eqs', type--vars'} where
Implementation
Syntax call
ListToCons[ expr ]
Input
a Mathematica expression expr
Output
the expression obtained from expr by replacing all Mathematica lists that are not lambda arguments
with the corresponding CFLP lists.
Implementation