File: bug4076.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (29 lines) | stat: -rw-r--r-- 669 bytes parent folder | download | duplicates (7)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
(* Check behavior of evar-evar subtyping problems in the presence of
   nested let-ins *)
(* Expected time < 2.00s *)

Set Implicit Arguments.
Unset Strict Implicit.

Parameter f : forall P, forall (i : nat), P i -> P i.
Parameter P : nat -> Type.

Time Definition g (n : nat) (a0 : P n) : P n :=
  let a1  := f a0 in
  let a2  := f a1 in
  let a3  := f a2 in
  let a4  := f a3 in
  let a5  := f a4 in
  let a6  := f a5 in
  let a7  := f a6 in
  let a8  := f a7 in
  let a9  := f a8 in
  let a10 := f a9 in 
  let a11 := f a10 in
  let a12 := f a11 in
  let a13 := f a12 in
  let a14 := f a13 in
  let a15 := f a14 in
  let a16 := f a15 in
  let a17 := f a16 in
  a17.