peano_naturals.v: get rid of universe N #1635
Annotations
1 error
|
Run coq-community/docker-coq-action@v1:
theories/Classes/theory/integers.v#L151
Unable to satisfy the following constraints:
In environment:
H : Funext
H0 : Univalence
Z : Type
Aap : Apart Z
Aplus : Plus Z
Amult : Mult Z
Azero : Zero Z
Aone : One Z
Anegate : Negate Z
Ale : Le Z
Alt : Lt Z
U : IntegersToRing Z
H1 : Integers Z
N : Type
Aap0 : Apart N
Aplus0 : Plus N
Amult0 : Mult N
Azero0 : Zero N
Aone0 : One N
Ale0 : Le N
Alt0 : Lt N
U0 : NaturalsToSemiRing N
H2 : Naturals N
x : Z
?Aap : "Apart N"
?Aplus : "Plus N"
?Amult : "Mult N"
?Azero : "Zero N"
?Aone : "One N"
?Ale : "Le N"
?Alt : "Lt N"
?U : "NaturalsToSemiRing N"
?H1 : "Naturals N"
?Aap0 : "Apart (NatPair.Z N)"
?Aplus0 : "Plus (NatPair.Z N)"
?Amult0 : "Mult (NatPair.Z N)"
?Azero0 : "Zero (NatPair.Z N)"
?Aone0 : "One (NatPair.Z N)"
?Anegate : "Negate (NatPair.Z N)"
?Ale0 : "Le (NatPair.Z N)"
?Alt0 : "Lt (NatPair.Z N)"
?U0 : "IntegersToRing (NatPair.Z N)"
?H : "Integers (NatPair.Z N)"
?U0 : "NaturalsToSemiRing N"
?IntAbs : "IntAbs (NatPair.Z N) N"
?Aplus1 : "Plus (NatPair.Z N)"
?Amult1 : "Mult (NatPair.Z N)"
?Azero1 : "Zero (NatPair.Z N)"
?Aone1 : "One (NatPair.Z N)"
?Anegate0 : "Negate (NatPair.Z N)"
?H0 : "IsRing (NatPair.Z N)"
Command exited with non-zero status 1
|
The logs for this run have expired and are no longer available.
Loading