peano_naturals.v: get rid of universe N #1633
Annotations
1 error
|
Run coq-community/docker-coq-action@v1:
theories/Classes/theory/naturals.v#L144
Unable to satisfy the following constraints:
In environment:
H : Funext
H0 : Univalence
N : Type@{U}
Aap : Apart@{U U} N
Aplus : Plus@{U} N
Amult : Mult@{U} N
Azero : Zero@{U} N
Aone : One@{U} N
Ale : Le@{U U} N
Alt : Lt@{U U} N
U : NaturalsToSemiRing@{U U} N
H1 : Naturals@{U U U U U U U U} N
Q := fun s : Operations@{HoTT.Classes.theory.naturals.2049 U} =>
forall P : s -> Type@{HoTT.Classes.theory.naturals.2050},
P 0 -> (forall n : s, P n -> P (1 + n)) -> forall n : s, P n
: Operations@{HoTT.Classes.theory.naturals.2049 U} ->
Type@{HoTT.Classes.theory.naturals.2066}
X : Zero@{U} nat
X0 : Lt@{U U} nat
?Aap0 : "Apart@{U U} nat"
?Aplus0 : "Plus@{U} nat"
?Amult0 : "Mult@{U} nat"
?Azero0 : "Zero@{U} nat"
?Aone0 : "One@{U} nat"
?Ale0 : "Le@{U U} nat"
?Alt0 : "Lt@{U U} nat"
?U0 : "NaturalsToSemiRing@{U U} nat"
?H2 : "Naturals@{U U U U U U U U} nat"
Command exited with non-zero status 1
|
The logs for this run have expired and are no longer available.
Loading