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

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

Process completed with exit code 1.

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

Unexpected input(s) 'name', 'authToken', 'extraPullNames', valid inputs are ['extra_nix_config', 'github_access_token', 'install_url', 'install_options', 'nix_path']

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/

Unable to delete artifact "alectryon-html"; the artifact was not found.

Unable to delete artifact "workspace-8.17"; the artifact was not found.

Unable to delete artifact "file-dep-graphs"; the artifact was not found.

Unable to delete artifact "timing-html"; the artifact was not found.

Unable to delete artifact "workspace-dev"; the artifact was not found.

Unable to delete artifact "coqdoc-html"; the artifact was not found.

Unable to delete artifact "dep-graphs"; the artifact was not found.