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

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

bool -> bool

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

Logical : Type := Unit ->? Unit

Pred : Type -> Type := \ a : Type . a_v-1 ->? Unit

Unit : Type

__*__ : +Type -> +Type -> Type

__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

__-->?__ : -Type -> +Type -> Type < __->?__

__->__ : -Type -> +Type -> Type < __->?__

__->?__ : -Type -> +Type -> Type

bool

: Type

%[type bool

::= True : bool

False : bool]%

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

False : bool %(construct bool)%

True : bool %(construct bool)%

__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__when__else__

: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

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

b : bool -> bool

%(op)%

= ((\ (var x : bool) .! (var x : bool)) : bool -> 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

bottom : forall a : Type . a_v-1 %(fun)%

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

false : Unit %(fun)%

not__ : ? Unit ->? Unit %(fun)%

notA

: bool

%(op)%

= ((case (op a : bool) of

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

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

bool) as

bool

true : Unit %(fun)%

�__ : ? Unit ->? Unit %(fun)%

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

type bool

::= True : bool

False : bool %(ga_bool)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op a : bool, (op True : bool) as bool) %(def_a)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op notA : bool,

((case (op a : bool) of

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

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

bool) as

bool) %(def_notA)%

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

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

(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

(op b : bool -> bool,

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

bool -> bool) %(def_b)%