Atom
inl(*); inr(*) fi ; x1@1/x2@1,x1@1. InjCase(if x1@1=1 inl(*) ; inr(*) fi ; body(x2;x1@2;x2@1); cont(z)); cont(z)); _. cont(z))| No other cites to report in MarkB_generic | |
| case_pattern2 | Def < a, inl < < "a", b > , c, 1 > > = > body(a;b;c) cont(x,z) == x/x2,x1. InjCase(x1; x1@0. x1@0/x2@0,x1@1. x2@0/x2@0,x1@2. InjCase(if x2@0="a"Atominl(*); inr(*) fi ; x1@1/x2@1,x1@1. InjCase(if x1@1=1 inl(*) ; inr(*) fi ; body(x2;x1@2;x2@1); cont(z)); cont(z)); _. cont(z)) |
| Syntax: | < a, inl < < "a", b > , c, 1 > > = > body(a;b;c) cont | has structure: | case_pattern2(a,b,c.body(a;b;c); cont) |
About:
 |  |  |  |  |
 |  |  |  |  |  |