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 vc qimp? | |
| case_vc_qimp | Def Case vc_qimp(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 vc_qimp(x) = > body(x) cont | has structure: | case_vc_qimp(x.body(x); cont) |
About:
 |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |