x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1])
"?" ; h.t h
A:Type, l:A List. ||l||
1 
hd(l) 
AA:Type, l:A List
. hd(l) A nil ; h.t tA:Type, l:A List. tl(l) A List| Who Cites case relname other? | |
| case_relname_other | Def Case x = > body(x) cont(x1,z) == (x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1]) |
| 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)) |
| Syntax: | Case x = > body(x) cont | has structure: | case_relname_other(x.body(x); cont) |
About:
 |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |