aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/PPFix.v
blob: 833eb3ad1cef9fff1433fbcf3cc068419826add5 (plain)
1
2
3
4
5
6
7
8
9

(* To test PP of fixpoints *)
Require Import Arith.
Check fix a(n: nat): n<5 -> nat :=
  match n return n<5 -> nat with
    | 0 => fun _ => 0
    | S n => fun h => S (a n (lt_S_n _ _ (lt_S _ _ h)))
  end.