---

Definition: switch
Switch(t) b ==  b t

Definition: switch_case
Case v => case cont ==  λx.if (x =z v) then case else cont x fi 

Definition: switch_default
Default => body EndSwitch ==  λx.body

Definition: switch_done
EndSwitch ==  λx.!undefined

Definition: case
Case(value) body ==  body value value

Definition: case_default
Default => body ==  λvalue,value. body

Definition: case_pair
<x,y> => body[x; y] ==  λvalue,cont. let x,y = value in body[x; y]

Definition: case_inl
inl(x) => body[x] cont ==  λvalue,contvalue. case value of inl(x) => body[x] | inr(_) => cont contvalue contvalue

Definition: case_inr
inr(x) => body[x] cont ==  λvalue,contvalue. case value of inl(_) => cont contvalue contvalue | inr(x) => body[x]

Definition: case_cons
x::y =>
    body[x; y]
cont ==
  λvalue,contvalue. rec-case(value) of [] => cont contvalue contvalue | hd::tl => f.body[hd; tl]

Definition: case_nil
[] => body cont ==  λvalue,contvalue. rec-case(value) of [] => body | hd::tl => f.cont contvalue contvalue

Definition: case_it
⋅ => body ==  λvalue,contvalue. body

Definition: case_bind
x:body ==  body



Home Index