type bool ::= True | False

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

op notA : bool =

case (op a : bool) of

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

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

as 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)

as bool

op b : bool -> bool =

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

%% 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)%