blob: 2d20511a04ab73331549f181ef160451f64862d5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* -*- coq-prog-args: ("-noinit"); -*- *)
Require Import Coq.Init.Notations.
Notation "x -> y" := (forall _ : x, y).
Inductive eq {A:Type} (a:A) : A -> Prop := eq_refl : eq a a.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Printing Universes.
(* Constructors for an inductive with indices *)
Module WithIndex.
Inductive foo@{i} : (Prop -> Prop) -> Prop := mkfoo: foo (fun x => x).
Monomorphic Universes i j.
Monomorphic Constraint i < j.
Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _.
End WithIndex.
|
