equal
deleted
inserted
replaced
102 normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]" |
102 normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]" |
103 |
103 |
104 normal_form "last[a,b,c]" |
104 normal_form "last[a,b,c]" |
105 normal_form "last([a,b,c]@xs)" |
105 normal_form "last([a,b,c]@xs)" |
106 |
106 |
107 (* FIXME |
107 normal_form "max 0 x" |
108 won't work since it relies on |
|
109 polymorphically used ad-hoc overloaded function: |
|
110 normal_form "max 0 (0::nat)" |
|
111 *) |
|
112 |
108 |
113 text {* |
109 text {* |
114 Numerals still take their time\<dots> |
110 Numerals still take their time\<dots> |
115 *} |
111 *} |
116 |
112 |