| No other cites to report in StandardLib |
|
enum1_switch | Def enum1_switch(value;el1;el2;el3)
Def == Switch(value)
Def == Case enum1_el1 => el1
Def == Case enum1_el2 => el2
Def == Case enum1_el3 => el3
Def == EndSwitch |
|
switch_done | Def EndSwitch(x) == !undefined |
|
enum1_el3 | Def enum1_el3 == 2 |
| | Thm* enum1_el3 enum1() |
| | Thm* enum1_el3 |
|
switch_case | Def Case v => case cont(x) == if x=v case else cont(x) fi |
|
enum1_el2 | Def enum1_el2 == 1 |
| | Thm* enum1_el2 enum1() |
| | Thm* enum1_el2 |
|
enum1_el1 | Def enum1_el1 == 0 |
| | Thm* enum1_el1 enum1() |
| | Thm* enum1_el1 |
|
switch | Def Switch(t) b == b(t) |
|
eq_int | Def i=j == if i=j true ; false fi |
| | Thm* i,j:. (i=j) |