File: bug_11722.v

package info (click to toggle)
coq-doc 8.20.0-2
  • links: PTS, VCS
  • area: non-free
  • in suites: forky, sid, trixie
  • size: 46,708 kB
  • sloc: ml: 234,429; sh: 4,686; python: 3,359; ansic: 2,644; makefile: 842; lisp: 172; javascript: 87; xml: 24; sed: 2
file content (20 lines) | stat: -rw-r--r-- 410 bytes parent folder | download | duplicates (5) 
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@{_}.