ADT TypeBodyCaml [ ] INITIALS tbCaml : LString * String * LTypeExprCaml * LTypeRepCaml * LConstraintTypeCaml -> TypeBodyCaml CONSTRUCTORS SELECTORS StringOfParamsTypeCaml:LString -> String StringOfTypeBodyCaml: TypeBodyCaml(i) -> String EQ_TypeBodyCaml(c): TypeBodyCaml(i) * TypeBodyCaml(i) -> BOOL AXIOMS StringOfParamsTypeCaml(nil_LString)="" StringOfParamsTypeCaml(cons_LString(s1,nil_LString))= concat_String("'", concat_String(s1," ")) StringOfParamsTypeCaml(cons_LString(s1,cons_LString(s2,t)))= concat_String("'", concat_String(s1, concat_String(",",StringOfParamsTypeCaml(cons_LString(s2,t))))) StringOfTypeBodyCaml(tbCaml(L1,S2,L3,L4,L5))= if AND(AND(isEmptyList_LTypeExprCaml(L3),isEmptyList_LTypeRepCaml(L4)),isEmptyList_LConstraintTypeCaml(L5)) then concat_String(StringOfParamsTypeCaml(L1),S2) else concat_String(StringOfParamsTypeCaml(L1), concat_String(S2, concat_String("=", concat_String(StringOfLTypeExprCaml(L3," "), concat_String(StringOfLTypeRepCaml(L4," "), concat_String(" ",StringOfLConstraintTypeCaml(L5))))))) fi EQ_TypeBodyCaml(tbCaml(L1,S2,L3,L4,L5),tbCaml(L6,S7,L8,L9,L10)) = AND(EQ_LString(L1,L6),AND(EQ_String(S2,S7),AND(EQ_LTypeExprCaml(L3,L8),AND(EQ_LTypeRepCaml(L4,L9),EQ_LConstraintTypeCaml(L5,L10)))))