| Who Cites rel arg typ? |
|
rel_arg_typ | Def rel_arg_typ(rn;i;de) == Case(rn) Case eq(Q) = > Q Case R = > (de.rel(R))[i] Default = > False |
|
case_default |
Def Default = > body(value,value) == body |
|
sig_rel |
Def t.rel == 2of(t) |
|
select |
Def l[i] == hd(nth_tl(i;l)) |
| |
Thm* A:Type, l:A List, n:. 0n n < ||l|| l[n] A |
|
case_relname_other |
Def Case x = > body(x) cont(x1,z)
== (x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1]) |
|
case_relname_eq |
Def Case eq(x) = > body(x) cont(x1,z)
== InjCase(x1; x2. body(x2); _. cont(z,z)) |
|
case |
Def Case(value) body == body(value,value) |
|
pi2 |
Def 2of(t) == t.2 |
| |
Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p)) |
|
nth_tl |
Def nth_tl(n;as) == if n0 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 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_inr |
Def inr(x) = > body(x) cont(value,contvalue)
== InjCase(value; _. cont(contvalue,contvalue); x. body(x)) |
|
le_int |
Def ij == j < i |
| | Thm* i,j:. (ij) |
|
lt_int |
Def i < j == if i < j true ; false fi |
| | Thm* i,j:. (i < j) |
|
bnot |
Def b == if b false else true fi |
| | Thm* b:. b |