File: bug_7723.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 (71 lines) | stat: -rw-r--r-- 1,444 bytes parent folder | download | duplicates (2)
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
Set Universe Polymorphism.

Module Segfault.

Inductive decision_tree : Type := .

Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B
  := match ls with
     | nil => None
     | cons x xs
       => match f x with
          | Some v => Some v
          | None => first_satisfying_helper f xs
          end
     end.

Axiom admit : forall {T}, T.
Definition dtree4 : option decision_tree :=
  match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil)
  with
  | Some _ => admit
  | None => admit
  end
.
Definition dtree'' := Eval vm_compute in dtree4. (* segfault *)

End Segfault.

Module OtherExample.

Definition bar@{i} := Type@{i}.
Definition foo@{i j} (x y z : nat) :=
  @id Type@{j} bar@{i}.
Eval vm_compute in foo.

End OtherExample.

Module LocalClosure.

Definition bar@{i} := Type@{i}.

Definition foo@{i j} (x y z : nat) :=
  @id (nat -> Type@{j}) (fun _ => Type@{i}).
Eval vm_compute in foo.

End LocalClosure.

Module QVar.

  Definition bar@{q|i|} := Type@{q|i}.

  Definition gbar@{q1 q2|i j|} := bar@{q2|i}.

  Eval vm_compute in gbar.

  Definition gprop := Eval vm_compute in gbar@{Type Prop|Set Set}.
  Check eq_refl : gprop = Prop.

End QVar.

Require Import Hurkens.
Polymorphic Inductive unit := tt.

Polymorphic Definition foo :=
  let x := id tt in (x, x, Type).

Lemma bad : False.
  refine (TypeNeqSmallType.paradox (snd foo) _).
  vm_compute.
  Fail reflexivity.
Abort.