Selected Objects
| def | switch |
Switch(t) b == b(t) |
| def | switch_case |
Case v => case cont(x) == if x= v case else cont(x) fi |
| def | switch_default |
Default => body EndSwitch(x) == body |
| def | switch_done |
EndSwitch(x) == !undefined |
| def | case |
Case(value) body == body(value,value) |
| def | case_default |
Default => body(value,value) == body |
| def | case_pair |
<x,y> => body(x;y)(value,cont) == value/x,y. body(x;y) |
| def | case_inl |
inl(x) => body(x) cont(value,contvalue)
== InjCase(value; x. body(x); _. cont(contvalue,contvalue)) |
| def | case_inr |
inr(x) => body(x) cont(value,contvalue)
== InjCase(value; _. cont(contvalue,contvalue); x. body(x)) |
| def | case_cons |
x::y => body(x;y) cont(value,contvalue)
== Case of value; nil cont(contvalue,contvalue) ; hd.tl body(hd;tl) |
| def | case_nil |
[] => body cont(value,contvalue)
== Case of value; nil body ; hd.tl cont(contvalue,contvalue) |
| def | case_it |
 => body(value,contvalue) == body |
| def | case_bind |
x:body == body |
| def | case_pattern1 |
<<"a", b>, c, 1> => body(b;c) cont(x,z)
== x/x2,x1.
== x2/x2@0,x1@0.
== InjCase(if x2@0="a" Atominl(*); inr(*) fi
== InjCase; x1/x2@1,x1@1.
== InjCase; InjCase(if x1@1=1 inl(*) ; inr(*) fi ; body(x1@0;x2@1); cont(z,z))
== InjCase; cont(z,z)) |
| def | pattern1 |
<<"a", b>, c, 1> == <<"a",b>,c,1> |
| def | case_pattern2 |
<a, inl <<"a", b>, c, 1>> => body(a;b;c) cont(x,z)
== x/x2,x1.
== InjCase(x1
== InjCase; x1@0. x1@0/x2@0,x1@1.
== InjCase; x1@0. x2@0/x2@0,x1@2.
== InjCase; x1@0. InjCase(if x2@0="a"Atominl(*); inr(*) fi
== InjCase; x1@0. InjCase; x1@1/x2@1,x1@1.
== InjCase; x1@0. InjCase; InjCase(if x1@1=1 inl(*) ; inr(*) fi
== InjCase; x1@0. InjCase; InjCase; body(x2;x1@2;x2@1)
== InjCase; x1@0. InjCase; InjCase; cont(z))
== InjCase; x1@0. InjCase; cont(z))
== InjCase; _. cont(z)) |
| def | pattern2 |
<a, inl <<"a", b>, c, 1>> == <a,inl(<<"a", b>, c, 1>)> |
| def | union1 |
union1() ==  +Type+(   ) |
| def | case_union1_term1 |
union1_term1(x) => body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z)) |
| def | union1_term1 |
union1_term1(x) == inl(x) |
| def | case_union1_term2 |
union1_term2(x) => body(x) cont(x1,z)
== InjCase(x1; _. cont(z,z); x2. InjCase(x2; x2@0. body(x2@0); _. cont(z,z))) |
| def | union1_term2 |
union1_term2(x) == inr(inl(x)) |
| def | case_union1_term3 |
union1_term3(x) => body(x) cont(x1,z)
== InjCase(x1; _. cont(z,z); x2. InjCase(x2; _. cont(z,z); x2@0. body(x2@0))) |
| def | union1_term3 |
union1_term3(x) == inr(inr(x)) |
| def | enum1 |
enum1() == 3 |
| def | enum1_switch |
enum1_switch(value;el1;el2;el3)
== Switch(value)
== Case enum1_el1 => el1
== Case enum1_el2 => el2
== Case enum1_el3 => el3
== EndSwitch |
| def | case_enum1_el1 |
enum1_el1 => body cont(x,z)
== InjCase(if x=0 inl(*) ; inr(*) fi ; body; cont(z,z)) |
| def | enum1_el1 |
enum1_el1 == 0 |
| def | case_enum1_el2 |
enum1_el2 => body cont(x,z)
== InjCase(if x=1 inl(*) ; inr(*) fi ; body; cont(z,z)) |
| def | enum1_el2 |
enum1_el2 == 1 |
| def | case_enum1_el3 |
enum1_el3 => body cont(x,z)
== InjCase(if x=2 inl(*) ; inr(*) fi ; body; cont(z,z)) |
| def | enum1_el3 |
enum1_el3 == 2 |
| COM | enum1_start |
------ begin enum1 ------ |
| THM | enum1_sq |
SQType(enum1()) |
| THM | eq_enum1_eq_true_intro |
 i,j:enum1(). i = j   ((i=j) ~ true) |
| THM | eq_enum1_eq_false_intro |
i,j:enum1().  i = j ((i=j) ~ false) |
| THM | enum1_cases |
i:enum1(). i = enum1_el1  i = enum1_el2 i = enum1_el3 |
| COM | enum1_finish |
------ end enum1 ------ |
| def | module1_type |
module1_type(prop) == tag:{i:| prop(i) }Unit+(module1_type( i.i = tag-1))
(recursive) |
| def | module1_tag |
t.tag == 1of(t) |
| def | module1_data |
t.data == 2of(t) |
| def | case_module1 |
module1(tag, data) => body(tag;data)(x,z) == x/x2,x1. body(x2;x1) |
| def | module1 |
module1(tag, data) == <tag,data> |