| Some definitions of interest. |
|
Knd | Def Knd == (IdLnk Id)+Id |
| | Thm* Knd Type |
|
ma-state | Def State(ds) == x:Id ds(x)?Top |
|
ma-valtype | Def ma-valtype(da; k) == da(k)?Top |
|
Id | Def Id == Atom  |
| | Thm* Id Type |
|
kindcase | Def kindcase(k;a.f(a);l,t.g(l;t))
Def == if islocal(k) f(act(k)) else g(lnk(k);tag(k)) fi |
| | Thm* B:Type, k:Knd, f:(Id B), g:(IdLnk Id B).
Thm* kindcase(k;a.f(a);l,t.g(l,t)) B |
|
actof | Def act(k) == outr(k) |
| | Thm* k:Knd. islocal(k)  act(k) Id |
|
fpf-single | Def x : v == <[x], x.v> |
|
islocal | Def islocal(k) ==  isl(k) |
| | Thm* k:Knd. islocal(k)  |