eb8bd58b5980a12a7f60ed40f9baf7263bc53946Jonathan von Schroederclass Type

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedervar t : Type

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elknerclass TYPE

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedertypes Pred __ : -Type -> Type;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder Unit : TYPE

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescuclasses a, b, c

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederclasses a, b, c < d;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder a < b

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedertype s : c

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederpred tt : s

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedervar x : s

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederprogram tt = \ x : s . ();

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederprogram

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder__ res __ (x : s, y : t) : s = x;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederfst (x : s, y : t) : s = x;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedersnd (x : s, y : t) : t = y;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederpred eq : s * s

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedertype s < ? s

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederprogram all (p : (? s)) : (? Unit) = eq (p, tt);

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederprogram And (x, y : (? Unit)) : (? Unit) = t1 () res t2 ();

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederprogram __ impl __ (x, y : (? Unit)) = eq (x, x And y);

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederprogram

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder__ or __ (x, y : (? Unit)) : (? Unit)

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder= all (\ r : (? Unit) . ((x impl r) res (y impl r)) impl r);

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederex (p : (? s)) : (? Unit)

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder= all (\ r : (? Unit) . all (\ x : s . p (x) impl r) impl r);

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederff () : (? Unit) = all (\ r : (? Unit) . r ());

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederforall x : t; y : t

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder%(..)%

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder. x = y;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedertype s

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederop a : (? s)

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedertype Data1 ::= a | b | c

eb8bd58b5980a12a7f60ed40f9baf7263bc53946Jonathan von Schroedertype Data2

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder ::= Cons21 (Data1; Data2) | Cons22 (Data2; Data1) | type Data1

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedertype Data3

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder ::= Cons31 (sel1 :? Data1; sel2 :? Data2) |

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder Cons32 (sel2 :? Data2; sel1 :? Data1)

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroedertype Data4

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder ::= Cons41 (sel1 :? Data1; sel2 :? Data2)? |

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder Cons42 (sel2 :? Data2; sel1 :? Data1)?

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder. true;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederforall x : s . e;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroederforall x : s . e;

c10f6b3d0617371b9759cd2db422832e44e74bd3Jonathan von Schroeder