blob: ab6262823c219fceb04ab9fe5e8470927df3d72c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Test the behaviour of hnf and simpl introduced in revision *)
Parameter n:nat.
Definition a:=0.
Eval simpl in (fix plus (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (p + m)
end) a a.
Eval hnf in match (plus (S n) O) with S n => n | _ => O end.
|
