BasicSpec.hascasl revision 7b47917488ffdd72119358c064c94e5dfc4f8fe3
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringclass TYPE : {x.x < t}
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringtype Pred __ : Type- -> Type; Unit:TYPE
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringclass a, b, c <d; a:b
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringprogram tt = \x: s . ()
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringprogram __res__ (x: s, y: t) : s = x ;
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringfst (x: s, y: t) : s = x ;
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringsnd (x: s, y: t) : t = y
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringprogram all (p: (?s)) : (?Unit) = eq(p, tt)
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringprogram And (x, y: (?Unit)) :(?Unit) = t1() res t2()
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringprogram __impl__ (x, y: (?Unit)) = eq(x, x And y)
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringprogram __or__ (x, y: (?Unit)) :(?Unit) = all(\r: (?Unit).
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering ((x impl r) res (y impl r)) impl r)
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering; ex (p: (?s)) :(?Unit) = all(\r: (?Unit).
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering all(\x:s. p(x) impl r) impl r)
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering; ff () :(?Unit) = all(\r: (?Unit). r())
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringforall x: t; y : t
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering op a: (?s); %[ Should be: op a:?s ]%
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering type Data1 ::= a | b | c;
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort Data1
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poettering type Data3 ::= Cons31 (sel1:?Data1; sel2:?Data2) | Cons32(sel2:?Data2; sel1:?
4943c1c94ba751c98763f4232b4350481b22c90aLennart Poettering type Data4 ::= Cons41 (sel1:?Data1; sel2:?Data2)? | Cons42(sel2:?Data2; sel1:?Data1)?
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringaxioms true ;forall x:s.e;