ADT ConstrDeclCaml [  ]

INITIALS
constantCDC : String                           -> ConstrDeclCaml
functionCDC : String * TypeExprCaml            -> ConstrDeclCaml

CONSTRUCTORS

SELECTORS
StringOfConstrDeclCaml:ConstrDeclCaml(i) -> String
EQ_ConstrDeclCaml(c): ConstrDeclCaml(i) * ConstrDeclCaml(i)  -> BOOL

AXIOMS

StringOfConstrDeclCaml(constantCDC(S1))=S1
StringOfConstrDeclCaml(functionCDC(S1,T2))=
  concat_String(S1,
  concat_String(" of ",StringOfTypeExprCaml(T2)))


EQ_ConstrDeclCaml(constantCDC(S1),constantCDC(S2)) = EQ_String(S1,S2)
EQ_ConstrDeclCaml(constantCDC(S1),functionCDC(S2,T3)) = FALSE
EQ_ConstrDeclCaml(functionCDC(S1,T2),constantCDC(S3)) = FALSE
EQ_ConstrDeclCaml(functionCDC(S1,T2),functionCDC(S3,T4)) = AND(EQ_String(S1,S3),EQ_TypeExprCaml(T2,T4))