lc http://www.openmath.org/cd/lc.ocd 2000-09-01 experimental 1999-08-20 1 0 Lambda Calculus Initial version: O. Caprotti type Attribution tag to denote type-judgement typecoerce Attribution tag to denote type-judgement with coercion PiType The type constructor of dependant function space. It binds the (type-attributed) variables in the body, that is an OpenMath object. mapsto The type constructor of non-dependant function space. The first n-1 children denote the types of the arguments, the last denotes the return type. Contrary to sts:mapsto, arguments cannot be variables but have to be OpenMath objects that map to ground OpenMath terms (they contain no variables). Lambda The abstraction constructor. It is followed by a list of variables and an OpenMath object.