Skip to content

chore(census): refresh the row of system-et (the Agda track is now on its main branch) #48

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Nov 10, 2026
+7 −9
Merged

chore(census): refresh the row of system-et (the Agda track is now on its main branch) #48

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/atlas/generated/az.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,7 @@
* `hyperpolymath/stateful-artefacts` — engineering; 4 own proof files, 23 detected declarations; provers: idris2 2, tla 2
* `hyperpolymath/statistikles` — theory; 4 own proof files, 22 detected declarations; provers: agda 4
* `catachresis-colloquium/stealth-glider-ecosystem` — engineering; 1 own proof files, 13 detected declarations; provers: idris2 1
* `hyperpolymath/system-et` — theory; 21 own proof files, 164 detected declarations; provers: lean 21
* `hyperpolymath/system-et` — theory; 86 own proof files, 612 detected declarations; provers: agda 65, lean 21

== T

Expand Down
2 changes: 1 addition & 1 deletion docs/atlas/generated/classes.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@
* `hyperpolymath/secret-types` — theory; 21 own proof files, 91 detected declarations; provers: agda 21
* `hyperpolymath/snifs` — theory; 3 own proof files, 43 detected declarations; provers: agda 2, idris2 1
* `hyperpolymath/statistikles` — theory; 4 own proof files, 22 detected declarations; provers: agda 4
* `hyperpolymath/system-et` — theory; 21 own proof files, 164 detected declarations; provers: lean 21
* `hyperpolymath/system-et` — theory; 86 own proof files, 612 detected declarations; provers: agda 65, lean 21
* `hyperpolymath/tangle` — theory; 3 own proof files, 61 detected declarations; provers: lean 3
* `hyperpolymath/trope-checker` — theory; 38 own proof files, 514 detected declarations; provers: agda 10, lean 12, idris2 16
* `hyperpolymath/tropical-types` — theory; 28 own proof files, 540 detected declarations; provers: lean 19, isabelle 9
Expand Down
2 changes: 1 addition & 1 deletion docs/atlas/generated/index.json
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion docs/atlas/generated/organisations.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,7 @@
* `hyperpolymath/ssg-collection` — engineering; 23 own proof files, 108 detected declarations; provers: lean 1, idris2 6, spark 13, other 3
* `hyperpolymath/stateful-artefacts` — engineering; 4 own proof files, 23 detected declarations; provers: idris2 2, tla 2
* `hyperpolymath/statistikles` — theory; 4 own proof files, 22 detected declarations; provers: agda 4
* `hyperpolymath/system-et` — theory; 21 own proof files, 164 detected declarations; provers: lean 21
* `hyperpolymath/system-et` — theory; 86 own proof files, 612 detected declarations; provers: agda 65, lean 21
* `hyperpolymath/tangle` — theory; 3 own proof files, 61 detected declarations; provers: lean 3
* `hyperpolymath/thunderbird-template-reloaded` — engineering; 10 own proof files, 74 detected declarations; provers: idris2 10
* `hyperpolymath/tlaiser` — engineering; 9 own proof files, 181 detected declarations; provers: idris2 9
Expand Down
6 changes: 2 additions & 4 deletions docs/catalogue/catalogue.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ verdicts.

|https://github.com/hyperpolymath/echo-types[hyperpolymath/echo-types] |161 |0 |agda 161 |1676 |0 |1 |0 |1 |`PROOF-STATUS.adoc`

|https://github.com/hyperpolymath/system-et[hyperpolymath/system-et] |86 |0 |agda 65, lean 21 |612 |0 |0 |0 |0 |`docs/status/PROOF-STATUS.adoc`

|https://github.com/hyperpolymath/ordinal-notation[hyperpolymath/ordinal-notation] |78 |0 |agda 78 |618 |0 |2 |0 |1 |`docs/status/PROOF-NEEDS.adoc`

|https://github.com/hyperpolymath/valence-shell[hyperpolymath/valence-shell] |64 |0 |agda 10, lean 16, rocq 12, isabelle 9, idris2 12, smt-atp 5 |996 |5 |1 |0 |9 |`PROOF-NEEDS.adoc`
Expand Down Expand Up @@ -54,8 +56,6 @@ verdicts.

|https://github.com/hyperpolymath/secret-types[hyperpolymath/secret-types] |21 |5 |agda 21 |91 |0 |0 |0 |0 |`PROOF-STATUS.adoc`

|https://github.com/hyperpolymath/system-et[hyperpolymath/system-et] |21 |0 |lean 21 |164 |0 |0 |0 |0 |`docs/status/PROOF-NEEDS.adoc`

|https://github.com/hyperpolymath/occupancy-types[hyperpolymath/occupancy-types] |20 |2 |agda 8, lean 6, idris2 6 |90 |0 |0 |0 |0 |`PROOF-STATUS.adoc`

|https://github.com/hyperpolymath/wokelang[hyperpolymath/wokelang] |18 |0 |lean 7, rocq 3, idris2 8 |418 |0 |0 |0 |0 |`PROOF-NEEDS.adoc`
Expand All @@ -72,8 +72,6 @@ verdicts.

|https://github.com/hyperpolymath/CompositionalDA.jl[hyperpolymath/CompositionalDA.jl] |15 |0 |agda 15 |63 |0 |1 |0 |0 |`proofs/PROOF-STATUS.md`

|https://github.com/metadatastician/hvn-dehallucinator[metadatastician/hvn-dehallucinator] |16 |7 |agda 10, idris2 1, tla 5 |203 |0 |0 |0 |0 |`docs/status/PROOF-STATUS.adoc`

|https://github.com/hyperpolymath/ExactCounts.jl[hyperpolymath/ExactCounts.jl] |15 |0 |agda 15 |236 |0 |1 |0 |6 |`proofs/PROOF-STATUS.md`

|https://github.com/hyperpolymath/jtv-lang[hyperpolymath/jtv-lang] |15 |0 |agda 5, lean 9, idris2 1 |287 |0 |0 |0 |0 |`verification/PROOF-STATUS.adoc`
Expand Down
2 changes: 1 addition & 1 deletion docs/catalogue/census/catalogue-rows.json
View file
Open in desktop

Large diffs are not rendered by default.

Loading