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
|
Require Import Classes.RelationClasses List Setoid.
Definition eqT (T : Type) := @eq T.
Set Universe Polymorphism.
Definition RowType := list Type.
Inductive Row : RowType -> Type :=
| RNil : Row nil
| RCons : forall T Ts, T -> Row Ts -> Row (T :: Ts).
Inductive RowTypeDecidable (P : forall T, relation T) `(H : forall T, Equivalence (P T))
: RowType -> Type :=
| RTDecNil : RowTypeDecidable P H nil
| RTDecCons : forall T Ts, (forall t0 t1 : T,
{P T t0 t1} + {~P T t0 t1})
-> RowTypeDecidable P H Ts
-> RowTypeDecidable P H (T :: Ts).
Set Printing Universes.
Fixpoint Row_eq (Ts : RowType)
: RowTypeDecidable (@eqT) _ Ts -> forall r1 r2 : Row Ts, {@eq (Row Ts) r1 r2} + {r1 <> r2}.
(* Toplevel input, characters 81-87:
Error:
In environment
Ts : RowType (* Top.53 Coq.Init.Logic.8 *)
r1 : Row (* Top.54 Top.55 *) Ts
r2 : Row (* Top.56 Top.57 *) Ts
The term "Row (* Coq.Init.Logic.8 Top.59 *) Ts" has type
"Type (* max(Top.58+1, Top.59) *)" while it is expected to have type
"Type (* Coq.Init.Logic.8 *)" (Universe inconsistency). *)
Abort.
|
