blob: 4a460a83fa8fc2d1105aaed53381f906be75cd6a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Test the behaviour of hnf and simpl introduced in revision *)
Variable 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.
|
