max
0 followers · 0 following
  • Joined on 2026-04-25
Repositories
7
 Projects Packages Public activity Starred repositories
max pushed to Dev_REL1 at max/cubical-transport-hott-lean4 2026-04-30 19:07:59 -05:00
50bb6660d6 REL1: typing rules + transp/comp derived theorems for .ind + Rust subst
4d6853a0ef REL1 Inductive.lean + Rust dispatch + 9 new smoke tests (25/25 + 46/46)
f27211f73f REL1 foundation: schema-based inductive + HIT CTypes (Lean side)
f9e79b7b0d REL1: design doc for schema-based inductive + HIT CTypes
Compare 4 commits »
max opened issue max/cubical-transport-hott-lean4#1 2026-04-30 15:47:11 -05:00
CType inductive-type encoding (for paideia K7 cubical Path)
max deleted branch master from max/octive-lean 2026-04-29 18:00:51 -05:00
max pushed to main at max/zigzag-engine 2026-04-29 18:00:50 -05:00
max deleted branch master from max/zigzag-engine 2026-04-29 18:00:50 -05:00
max created branch main in max/octive-lean 2026-04-29 18:00:50 -05:00
max pushed to main at max/octive-lean 2026-04-29 18:00:50 -05:00
max created branch main in max/zigzag-engine 2026-04-29 18:00:49 -05:00
max created branch main in max/cubical-transport-hott-lean4 2026-04-29 18:00:49 -05:00
max pushed to main at max/cubical-transport-hott-lean4 2026-04-29 18:00:49 -05:00
58330df245 Add NOTICE: AI tooling acknowledgement; proprietary rights stand on human-directed whole
5e9be0ffe2 Add proprietary LICENSE; move CI to .forgejo/workflows/, run cubical-test
92bd67ac4a Regenerate lake-manifest.json: package name cubicalTransport (was stale 'topolei')
d9f952fa6c Reorganize: move non-README docs into docs/ subfolder
8561e19467 Docs cleanup: archive PHASE1, accept ZIGZAG_PORT, fix stale paths
max deleted branch master from max/cubical-transport-hott-lean4 2026-04-29 18:00:49 -05:00
max pushed to master at max/octive-lean 2026-04-29 10:44:26 -05:00
23162fb93a Add README, CONTRIBUTING, editorconfig, gitattributes, justfile
max created branch master in max/octive-lean 2026-04-29 10:40:52 -05:00
max pushed to master at max/octive-lean 2026-04-29 10:40:52 -05:00
db79eb3fde Initial commit: Lean 4 reimplementation of GNU Octave
max created repository max/octive-lean 2026-04-29 10:40:38 -05:00
max pushed to master at max/cubical-transport-hott-lean4 2026-04-28 00:10:33 -05:00
58330df245 Add NOTICE: AI tooling acknowledgement; proprietary rights stand on human-directed whole
max pushed to master at max/cubical-transport-hott-lean4 2026-04-28 00:04:19 -05:00
5e9be0ffe2 Add proprietary LICENSE; move CI to .forgejo/workflows/, run cubical-test
max pushed to master at max/cubical-transport-hott-lean4 2026-04-28 00:00:02 -05:00
92bd67ac4a Regenerate lake-manifest.json: package name cubicalTransport (was stale 'topolei')
max pushed to master at max/cubical-transport-hott-lean4 2026-04-27 23:57:11 -05:00
d9f952fa6c Reorganize: move non-README docs into docs/ subfolder
max pushed to master at max/cubical-transport-hott-lean4 2026-04-27 23:52:17 -05:00
8561e19467 Docs cleanup: archive PHASE1, accept ZIGZAG_PORT, fix stale paths