aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/reduction.v
blob: c4592369f76e27d762fad513f58279978f17155b (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.