Lazy.hascasl.output revision b55cf4375478168316b212cbc7d261fb683645ff
type t
op f : ? t -> t
op g : t -> (? t)
op a, b : t
op c, d : ? t
. __=__
((op f : ? t -> t) (op a : t), (op g : t -> ? t) (op c : ? t))
%% Type Constructors -----------------------------------------------------
? : +Type -> Type
Logical : Type := ? Unit
Pred : -Type -> Type := \ a : -Type . a ->? Unit
Unit : Type
__*__ : +Type -> +Type -> Type
__*__*__ : +Type -> +Type -> +Type -> Type
__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type
__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
__-->?__ : -Type -> +Type -> Type < __->?__
__->__ : -Type -> +Type -> Type < __->?__
__->?__ : -Type -> +Type -> Type
t : Type
%% Assumptions -----------------------------------------------------------
__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=__ : forall a : Type . a * a ->? Unit %(fun)%
__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
__if__ : ? Unit * ? Unit ->? Unit %(fun)%
__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%
a : t %(op)%
b : t %(op)%
bottom : forall a : Type . a %(fun)%
c : ? t %(op)%
d : ? t %(op)%
def__ : forall a : Type . a ->? Unit %(fun)%
f : ? t -> t %(op)%
false : Unit %(fun)%
g : t -> ? t %(op)%
not__ : ? Unit ->? Unit %(fun)%
true : Unit %(fun)%
�__ : ? Unit ->? Unit %(fun)%
%% Sentences -------------------------------------------------------------
__=__ (f a, g c)