summaryrefslogtreecommitdiff
path: root/test-suite/output/reduction.v
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.