l:Pattern. right_ptn(l) 
Pattern| No mentions to report in GenAutomata | |
| right_ptn | Def right_ptn(l) == Case(l) Case ptn_pr( < x, y > ) = > y Default = > l |
| Thm* l:Pattern. right_ptn(l) Pattern | |
| case_default | Def Default = > body(value,value) == body |
| 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 | Def Case(value) body == body(value,value) |
About:
 |  |
 |  |  |  |