ADT BOOLExprCaml [  ]
/*  BOOLExprCaml : BOOL -> ExprCaml */

INITIALS

CONSTRUCTORS

SELECTORS
BOOLExprCaml_TRUE   :                                  -> ExprCaml
BOOLExprCaml_FALSE   :                                  -> ExprCaml
BOOLExprCaml_AND   : ExprCaml * ExprCaml              -> ExprCaml
BOOLExprCaml_OR   : ExprCaml * ExprCaml              -> ExprCaml
BOOLExprCaml_NOT   : ExprCaml                         -> ExprCaml
BOOLExprCaml_IMP   : ExprCaml * ExprCaml              -> ExprCaml
BOOLExprCaml_EQ_BOOL   : ExprCaml * ExprCaml              -> ExprCaml

isBOOL_TRUE:String->BOOL
isBOOL_FALSE:String->BOOL
isBOOL_AND:String->BOOL
isBOOL_OR:String->BOOL
isBOOL_NOT:String->BOOL
isBOOL_IMP:String->BOOL
isBOOL_EQ_BOOL:String->BOOL

AXIOMS

BOOLExprCaml_TRUE=constantEC(consCC("true"))
BOOLExprCaml_FALSE=constantEC(consCC("false"))
BOOLExprCaml_AND(E1,E2)=infixEC(E1,"&&",E2)
BOOLExprCaml_OR(E1,E2)=infixEC(E1,"||",E2)
BOOLExprCaml_NOT(E1)=funApp(valPathEC("not "),E1)
BOOLExprCaml_IMP(E1,E2)=BOOLExprCaml_OR(BOOLExprCaml_NOT(E1),E2)
BOOLExprCaml_EQ_BOOL(E1,E2)=infixEC(E1,"=",E2)

isBOOL_TRUE(s)=EQ_String(s,"TRUE")
isBOOL_FALSE(s)=EQ_String(s,"FALSE")
isBOOL_AND(s)=EQ_String(s,"AND")
isBOOL_OR(s)=EQ_String(s,"OR")
isBOOL_NOT(s)=EQ_String(s,"NOT")
isBOOL_IMP(s)=EQ_String(s,"IMP")
isBOOL_EQ_BOOL(s)=EQ_String(s,"EQ_BOOL")