equal
deleted
inserted
replaced
126 "_abs (Pair x y) t" => "%(x,y).t" |
126 "_abs (Pair x y) t" => "%(x,y).t" |
127 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
127 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
128 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
128 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
129 |
129 |
130 "SIGMA x:A. B" => "Sigma A (%x. B)" |
130 "SIGMA x:A. B" => "Sigma A (%x. B)" |
131 "A <*> B" => "Sigma A (_K B)" |
131 "A <*> B" => "Sigma A (%_. B)" |
132 |
132 |
133 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*) |
133 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*) |
134 (* works best with enclosing "let", if "let" does not avoid eta-contraction *) |
134 (* works best with enclosing "let", if "let" does not avoid eta-contraction *) |
135 print_translation {* |
135 print_translation {* |
136 let fun split_tr' [Abs (x,T,t as (Abs abs))] = |
136 let fun split_tr' [Abs (x,T,t as (Abs abs))] = |