icc http://www.openmath.org/cd/icc.ocd 2000-09-01 experimental 1 1 lc setname1 ICC Typing Attributes for OM Initial version: O. Caprotti (July 1, 1999) Revised by W.A. Naylor on 2000-02-02 to reflect the name change of setname, also adding CDUses. type Attribution tag to denote type-judgement typecoerce Attribution tag to denote type-judgement with coercion IndType Constructor for Inductive Types. Takes arguments the constructor functions for the inhabitants of the type and their signatures. 0 is the defining mathematical property for the symbolic type nat of the inductively defined natural numbers with 0 and succ as constructor functions.