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

bool : Type

op False : bool %(constructor)%

op True : bool %(constructor)%

op a : bool %[ = (op True : bool) ]%

op b : bool

%[ =

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

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

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

in

(op True : bool) ]%

op b : bool -> bool %[ = \ x : bool .! (var x : bool) ]%

op notA : bool

%[ =

case (op a : bool) of

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

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

type bool ::= False | True %(ga_bool)%

. a = True

. notA = case a of True -> False | False -> True

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

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