blob: d4bd5f48b2369bee7826b77152482fe07d66b8ce (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Require Import Program.
Set Universe Polymorphism.
Inductive paths@{i} (A : Type@{i}) (a : A) : A -> Type@{i} :=
idpath : paths A a a.
Inductive nat :=
| O : nat
| S : nat -> nat.
Axiom cheat : forall {A}, A.
Program Definition foo@{i} : forall x : nat, paths@{i} nat x x := _.
Next Obligation.
destruct x.
constructor.
apply cheat.
Defined. (* FIXED: Universe unbound error *)
Check foo@{_}.
|
