No subject

[Henry Cejtin]

In  case  7  of  figure  5  (translation),  I  again  suggest  that  we go to
consistently having the | both before and after the generic case.  I.e.,
        [ case y of ... | C z => e | ... ]x = ...

In the last case (#11) of figure 5 (translation), since X returns  a  binding
occurrence, it can't be the body of a let.

Also, you meant
        y2 = [ e2 ]
instead of
        y2 = e2
in the translation.

Also you forgot to say that y1 and y2 are fresh variables.

I.e., I claim that
        [ e1 handle z => e2 ] x
is
        let y1 = [ e1 ]
            y2 = X(y1, F(last(e1)), F(x))
        in y2
        end handle z => let y3 = [ e2 ]
                            y4 = X(y3, F(last(e2)), F(x))
                        in y4
                        end
        with y1, y2, y3 and y4 all fresh.