49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrenceclass Type

bd911976d51f102751848568ccf56592fd5f6d77Tinderbox User

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David Lawrencevar t:Type

0c27b3fe77ac1d5094ba3521e8142d9e7973133fMark Andrews

0c27b3fe77ac1d5094ba3521e8142d9e7973133fMark Andrewsclass TYPE : {x.x < t}

0c27b3fe77ac1d5094ba3521e8142d9e7973133fMark Andrews

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrencetype Pred __ : Type- -> Type; Unit:TYPE

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

28a8f5b0de57d269cf2845c69cb6abe18cbd3b3aMark Andrews

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrenceclass a, b, c

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrenceclass a, b, c <d; a:b

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayertype s:c

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayer

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrencepred tt : s

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayervar x : s

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayer

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayerprogram tt = \x: s . ()

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayer

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayerprogram __res__ (x: s, y: t) : s = x ;

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrencefst (x: s, y: t) : s = x ;

a13e9f894ce1fa80b4076a40ade53982d8e9d1d9Mukund Sivaramansnd (x: s, y: t) : t = y

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayerpred eq : s * s

a13e9f894ce1fa80b4076a40ade53982d8e9d1d9Mukund Sivaraman

a13e9f894ce1fa80b4076a40ade53982d8e9d1d9Mukund Sivaramantype s < ?s

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayer

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayerprogram all (p: (?s)) : (?Unit) = eq(p, tt)

e35c1bb3ecd9a6597360b9160b397c8053af69bfDanny Mayer

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrenceprogram And (x, y: (?Unit)) :(?Unit) = t1() res t2()

92ef1a9b9dbd48ecb507b42ac62c15afefdaf838David Lawrence

92ef1a9b9dbd48ecb507b42ac62c15afefdaf838David Lawrenceprogram __impl__ (x, y: (?Unit)) = eq(x, x And y)

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrenceprogram __or__ (x, y: (?Unit)) :(?Unit) = all(\r: (?Unit).

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence ((x impl r) res (y impl r)) impl r)

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence; ex (p: (?s)) :(?Unit) = all(\r: (?Unit).

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence all(\x:s. p(x) impl r) impl r)

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence; ff () :(?Unit) = all(\r: (?Unit). r())

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence;

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrenceforall x: t; y : t

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence%(..)%

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence. x = y

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence%[% [ ] % %[

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence]%

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence%[ ]%

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence]%

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

40f53fa8d9c6a4fc38c0014495e7a42b08f52481David Lawrence%[ ]%

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence sort s

0e1bef59f060f6442a93cb662b0313e8908500e1Bob Halley op a: (?s); %[ Should be: op a:?s ]%

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence type Data1 ::= a | b | c;

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort Data1

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence type Data3 ::= Cons31 (sel1:?Data1; sel2:?Data2) | Cons32(sel2:?Data2; sel1:?

49e558760e9c21a6b7c726ccf999a2711fd8eef9David LawrenceData1)

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence type Data4 ::= Cons41 (sel1:?Data1; sel2:?Data2)? | Cons42(sel2:?Data2; sel1:?Data1)?

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrenceaxioms true ;forall x:s.e;

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrenceforall x:s.e

49e558760e9c21a6b7c726ccf999a2711fd8eef9David Lawrence