BasicSpec.hascasl revision a030fdd60d67ac5b7fe898c4346a64f136807013
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksaclass TYPE < Type
9940047ec4fd0ef151dfddd4253534eafa8c900cEugen Kuksatype Pred __ : -Type -> Type; Unit:TYPE
9940047ec4fd0ef151dfddd4253534eafa8c900cEugen Kuksaclass a, b, c
9940047ec4fd0ef151dfddd4253534eafa8c900cEugen Kuksaclass a, b, c <d; a:b
9940047ec4fd0ef151dfddd4253534eafa8c900cEugen Kuksaprogram tt = \x: s . ()
9940047ec4fd0ef151dfddd4253534eafa8c900cEugen Kuksaprogram __res__ (x: s, y: t) : s = x ;
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksafst (x: s, y: t) : s = x ;
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksasnd (x: s, y: t) : t = y
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksapred eq : s * s
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksaprogram all (p: (?s)) : (?Unit) = eq(p, tt)
9940047ec4fd0ef151dfddd4253534eafa8c900cEugen Kuksaprogram And (x, y: (?Unit)) :(?Unit) = t1() res t2()
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksaprogram __impl__ (x, y: (?Unit)) = eq(x, x And y)
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksaprogram __or__ (x, y: (?Unit)) :(?Unit) = all(\r: (?Unit).
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa ((x impl r) res (y impl r)) impl r)
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa; ex (p: (?s)) :(?Unit) = all(\r: (?Unit).
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa all(\x:s. p(x) impl r) impl r)
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa; ff () :(?Unit) = all(\r: (?Unit). r())
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksaforall x: t; y : t
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa op a: (?s); %[ Should be: op a:?s ]%
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa type Data1 ::= a | b | c;
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort Data1
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa type Data3 ::= Cons31 (sel1:?Data1; sel2:?Data2) | Cons32(sel2:?Data2; sel1:?
4d437fdae7216cb88d5f093833b1c0166ef2a53bEugen Kuksa type Data4 ::= Cons41 (sel1:?Data1; sel2:?Data2)? | Cons42(sel2:?Data2; sel1:?Data1)?
9940047ec4fd0ef151dfddd4253534eafa8c900cEugen Kuksaaxioms true ;forall x:s.e;