| | Some definitions of interest. |
|
| Kind-deq | Def KindDeq == union-deq(IdLnk Id;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq) |
|
| Knd | Def Knd == (IdLnkId)+Id |
| | | Thm* Knd  Type |
|
| IdLnk | Def IdLnk == IdId |
| | | Thm* IdLnk Type |
|
| idlnk-deq | Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq)) |
|
| ma-state | Def State(ds) == x:Id  ds(x)?Top |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| fpf-sub | Def f  g ==  x:A.  x dom(f)   x dom(g) & f(x) = g(x) B(x) |
|
| id-deq | Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq) |
|
| product-deq | Def product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)> |
|
| assert | Def b == if b True else False fi |
| | | Thm* b: . b Prop |
|
| fpf | Def a:A fp-> B(a) == d:A Lista:{a:A| (a d) }B(a) |
| | | Thm* A:Type, B:(AType). a:A fp-> B(a) Type |
|
| fpf-cap | Def f(x)?z == if x dom(f) f(x) else z fi |
|
| fpf-ap | Def f(x) == 2of(f)(x) |
|
| fpf-dom | Def x dom(f) == deq-member(eq;x;1of(f)) |
|
| locl | Def locl(a) == inr(a) |
| | | Thm* a:Id. locl(a) Knd |
|
| pi1 | Def 1of(t) == t.1 |
| | | Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |
|
| pi2 | Def 2of(t) == t.2 |
| | | Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p)) |
|
| rcv | Def rcv(l; tg) == inl(<l,tg>) |
| | | Thm* l:IdLnk, tg:Id. rcv(l; tg) Knd |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
