| Some definitions of interest. |
|
ma-frame-compatible | Def ma-frame-compatible(A; B)
Def == kx:(Knd Id).
Def == ( kx dom(1of(2of(2of(2of(2of(A))))))
Def == (
Def == ( 2of(kx) dom(1of(2of(2of(2of(2of(2of(2of(A))))))))
Def == (
Def == ( 2of(kx) dom(1of(2of(2of(2of(2of(2of(2of(B))))))))
Def == (
Def == ( deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(
Def == ( deq-member(KindDeq;1of(kx);1of(B)))))))(2of(kx))))
Def == & ( kx dom(1of(2of(2of(2of(2of(B))))))
Def == & (
Def == & ( 2of(kx) dom(1of(2of(2of(2of(2of(2of(2of(B))))))))
Def == & (
Def == & ( 2of(kx) dom(1of(2of(2of(2of(2of(2of(2of(A))))))))
Def == & (
Def == & ( deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(
Def == & ( deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx)))) |
|
msga | Def MsgA
Def == ds:x:Id fp-> Type
Def == da:a:Knd fp-> Type
Def == x:Id fp-> ds(x)?Void a:Id fp-> State(ds) ma-valtype(da; locl(a)) Prop
Def == kx:Knd Id fp-> State(ds) ma-valtype(da; 1of(kx)) ds(2of(kx))?Void
Def == kl:Knd IdLnk fp-> (tg:Id
Def == kl:Knd IdLnk fp-> ( State(ds) ma-valtype(da; 1of(kl))
Def == kl:Knd IdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
Def == x:Id fp-> Knd List ltg:IdLnk Id fp-> Knd List Top |
| | Thm* MsgA Type{i'} |