peano_naturals.v: get rid of universe N #1635
jdchristensenci.yml
on: pull_request
Matrix: coqchk
Matrix: install
doc-alectryon
0s
doc-dep-graphs
0s
doc-coqdoc
0s
doc-timing
0s
delete-artifacts
5s
Annotations
4 errors and 10 warnings
|
build (dev, --warnings):
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
|
|
nix
Process completed with exit code 1.
|
|
build (latest):
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
|
|
build (supported):
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
|
|
nix
Unexpected input(s) 'name', 'authToken', 'extraPullNames', valid inputs are ['extra_nix_config', 'github_access_token', 'install_url', 'install_options', 'nix_path']
|
|
delete-artifacts
The following actions uses node12 which is deprecated and will be forced to run on node16: geekyeggo/delete-artifact@v1. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
delete-artifacts
Unable to delete artifact "alectryon-html"; the artifact was not found.
|
|
delete-artifacts
Unable to delete artifact "workspace-8.17"; the artifact was not found.
|
|
delete-artifacts
Unable to delete artifact "file-dep-graphs"; the artifact was not found.
|
|
delete-artifacts
Unable to delete artifact "timing-html"; the artifact was not found.
|
|
delete-artifacts
Unable to delete artifact "workspace-dev"; the artifact was not found.
|
|
delete-artifacts
Unable to delete artifact "coqdoc-html"; the artifact was not found.
|
|
delete-artifacts
Unable to delete artifact "dep-graphs"; the artifact was not found.
|
|
delete-artifacts
Unable to delete artifact "workspace-latest"; the artifact was not found.
|