97 norm_by_eval "case n of None \<Rightarrow> True | Some((x,y),(u,v)) \<Rightarrow> False" |
97 norm_by_eval "case n of None \<Rightarrow> True | Some((x,y),(u,v)) \<Rightarrow> False" |
98 norm_by_eval "let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)" |
98 norm_by_eval "let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)" |
99 norm_by_eval "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))" |
99 norm_by_eval "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))" |
100 norm_by_eval "last[a,b,c]" |
100 norm_by_eval "last[a,b,c]" |
101 |
101 |
102 ( |
102 (* |
103 won't work since it relies on |
103 won't work since it relies on |
104 polymorphically used ad-hoc overloaded function: |
104 polymorphically used ad-hoc overloaded function: |
105 norm_by_eval "max 0 (0::nat)" |
105 norm_by_eval "max 0 (0::nat)" |
106 *) |
106 *) |
107 |
107 |
108 text (* |
108 text (* |
109 Numerals still take their time\<dots> |
109 Numerals still take their time\<dots> |
110 *) |
110 *) |
111 |
111 |
112 end |
112 end |
113 |
|
114 |
|