equal
deleted
inserted
replaced
30 {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init |
30 {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init |
31 |
31 |
32 (* Sum types *) |
32 (* Sum types *) |
33 fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT]) |
33 fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT]) |
34 fun mk_sumcase TL TR T l r = |
34 fun mk_sumcase TL TR T l r = |
35 Const (@{const_name sum.sum_case}, |
35 Const (@{const_name sum.case_sum}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r |
36 (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r |
|
37 |
36 |
38 val App = curry op $ |
37 val App = curry op $ |
39 |
38 |
40 fun mk_inj ST n i = |
39 fun mk_inj ST n i = |
41 access_top_down |
40 access_top_down |