| Who Cites R async? |
|
R_async | Def asyncR(E) == swap adjacent[ loc(E)(x) = loc(E)(y) & ![](FONT/not.png) (is-send(E)(x)) & ![](FONT/not.png) (is-send(E)(y)) (is-send(E)(x)) & (is-send(E)(y))] |
| | Thm* E:EventStruct. asyncR(E) (|E| List)![](FONT/dash.png) (|E| List)![](FONT/dash.png) Prop |
|
event_is_snd | Def is-send(E) == 1of(2of(2of(2of(2of(E))))) |
| | Thm* E:EventStruct. is-send(E) |E|![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/bool.png) |
|
lbl | Def Label == {p:Pattern| ground_ptn(p) } |
| | Thm* Label Type |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
swap_adjacent | Def swap adjacent[P(x;y)](L1,L2) == i: (||L1||-1). P(L1[i];L1[(i+1)]) & L2 = swap(L1;i;i+1) A List |
| | Thm* A:Type, P:(A![](FONT/dash.png) A![](FONT/dash.png) Prop). swap adjacent[P(x,y)] (A List)![](FONT/dash.png) (A List)![](FONT/dash.png) Prop |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
lelt | Def i j < k == i j & j < k |
|
le | Def A B == B < A |
| | Thm* i,j: . (i j) Prop |
|
not | Def A == A ![](FONT/eq.png) False |
| | Thm* A:Prop. ( A) Prop |
|
event_loc | Def loc(E) == 1of(2of(2of(2of(E)))) |
| | Thm* E:EventStruct. loc(E) |E|![](FONT/dash.png) Label |
|
carrier | Def |S| == 1of(S) |
| | Thm* S:Structure. |S| Type |
|
pi2 | Def 2of(t) == t.2 |
| | Thm* A:Type, B:(A![](FONT/dash.png) Type), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
pi1 | Def 1of(t) == t.1 |
| | Thm* A:Type, B:(A![](FONT/dash.png) Type), p:(a:A B(a)). 1of(p) A |
|
ground_ptn | Def ground_ptn(p) == Case(p) Case ptn_var(v) = > false Case ptn_pr( < x, y > ) = > ground_ptn(x)![](FONT/and.png) ground_ptn(y) Default = > true (recursive) |
| | Thm* p:Pattern. ground_ptn(p) ![](FONT/bool.png) |
|
ptn | Def Pattern == rec(T.ptn_con(T)) |
| | Thm* Pattern Type |
|
swap | Def swap(L;i;j) == (L o (i, j)) |
| | Thm* T:Type, L:T List, i,j: ||L||. swap(L;i;j) T List |
|
permute_list | Def (L o f) == mklist(||L||; i.L[(f(i))]) |
| | Thm* T:Type, L:T List, f:( ||L||![](FONT/dash.png) ![](FONT/then_med.png) ||L||). (L o f) T List |
|
select | Def l[i] == hd(nth_tl(i;l)) |
| | Thm* A:Type, l:A List, n: . 0 n ![](FONT/eq.png) n < ||l|| ![](FONT/eq.png) l[n] A |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l|| ![](FONT/int.png) |
| | Thm* ||nil|| ![](FONT/int.png) |
|
case_default | Def Default = > body(value,value) == body |
|
band | Def p![](FONT/and.png) q == if p q else false fi |
| | Thm* p,q: . (p![](FONT/and.png) q) ![](FONT/bool.png) |
|
case_lbl_pair | Def Case ptn_pr( < x, y > ) = > body(x;y) cont(x1,z) == InjCase(x1; _. cont(z,z); x2. InjCase(x2; _. cont(z,z); x2@0. InjCase(x2@0; _. cont(z,z); x2@1. x2@1/x3,x2@2. body(x3;x2@2)))) |
|
case_ptn_var | Def Case ptn_var(x) = > body(x) cont(x1,z) == ( x1.inr(x2) = > ( x1.inr(x2) = > ( x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x1]) |
|
case | Def Case(value) body == body(value,value) |
|
ptn_con | Def ptn_con(T) == Atom+ +Atom+(T T) |
| | Thm* T:Type. ptn_con(T) Type |
|
flip | Def (i, j)(x) == if x= i j ;x= j i else x fi |
| | Thm* k: , i,j: k. (i, j) k![](FONT/dash.png) ![](FONT/then_med.png) k |
|
nth_tl | Def nth_tl(n;as) == if n![](FONT/le.png) 0 as else nth_tl(n-1;tl(as)) fi (recursive) |
| | Thm* A:Type, as:A List, i: . nth_tl(i;as) A List |
|
hd | Def hd(l) == Case of l; nil "?" ; h.t h |
| | Thm* A:Type, l:A List. ||l|| 1 ![](FONT/eq.png) hd(l) A |
| | Thm* A:Type, l:A List . hd(l) A |
|
tl | Def tl(l) == Case of l; nil nil ; h.t t |
| | Thm* A:Type, l:A List. tl(l) A List |
|
case_inl | Def inl(x) = > body(x) cont(value,contvalue) == InjCase(value; x. body(x); _. cont(contvalue,contvalue)) |
|
case_inr | Def inr(x) = > body(x) cont(value,contvalue) == InjCase(value; _. cont(contvalue,contvalue); x. body(x)) |
|
mklist | Def mklist(n;f) == primrec(n;nil; i,l. l @ [(f(i))]) |
| | Thm* T:Type, n: , f:( n![](FONT/dash.png) T). mklist(n;f) T List |
|
primrec | Def primrec(n;b;c) == if n= 0 b else c(n-1,primrec(n-1;b;c)) fi (recursive) |
| | Thm* T:Type, n: , b:T, c:( n![](FONT/dash.png) T![](FONT/dash.png) T). primrec(n;b;c) T |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j) ![](FONT/bool.png) |
|
le_int | Def i![](FONT/le.png) j == ![](FONT/not.png) j < i |
| | Thm* i,j: . (i![](FONT/le.png) j) ![](FONT/bool.png) |
|
append | Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive) |
| | Thm* T:Type, as,bs:T List. (as @ bs) T List |
|
lt_int | Def i < j == if i < j true ; false fi |
| | Thm* i,j: . (i < j) ![](FONT/bool.png) |
|
bnot | Def ![](FONT/not.png) b == if b false else true fi |
| | Thm* b: . ![](FONT/not.png) b ![](FONT/bool.png) |