type bool ::= True | False;

op a : bool = True;

op notA : bool = case a of True -> False | False -> True;

op b : bool = let x = True; y = False; z = x in True;

op b : bool -> bool = \ x .! x;

%% Type Constructors -----------------------------------------------------

bool

: Type

%[type bool ::=

True : bool

False : bool]%

%% Assumptions -----------------------------------------------------------

False : bool %(construct bool)%

True : bool %(construct bool)%

a : bool %(op)% = (op True : bool) as bool

b

: bool -> bool

%(op)% = (\ (var x : bool) .! (var x : bool)) as bool -> bool

: bool

%(op)% =

(let (var x : bool) = (op True : bool);

(var y : bool) = (op False : bool);

(var z : bool) = (var x : bool)

in

(op True : bool))

as bool

notA

: bool

%(op)% =

(case (op a : bool) of

(op True : bool) -> (op False : bool) |

(op False : bool) -> (op True : bool))

as bool

%% Sentences -------------------------------------------------------------

type bool ::=

True : bool

False : bool %(ga_bool)%

a = (True as bool) %(def_a)%

notA = ((case a of True -> False | False -> True) as bool)

%(def_notA)%

(op b : bool) = ((let x = True; y = False; z = x in True) as bool)

%(def_b)%

(op b : bool -> bool) = ((\ x .! x) as bool -> bool) %(def_b)%