max
0 followers · 0 following
  • Joined on 2026-04-25
Repositories
7
 Projects Packages Public activity Starred repositories
max pushed tag pre-alpha-0.0.1 to max/terainia 2026-05-23 00:34:13 -05:00
max created branch main in max/terainia 2026-05-23 00:34:08 -05:00
max pushed to main at max/terainia 2026-05-23 00:34:08 -05:00
3a4ae970b2 pre-alpha 0.0.1 — initial multiplayer voxel sandbox
max created repository max/terainia 2026-05-23 00:33:59 -05:00
max created branch master in max/lean4-htt 2026-05-22 14:10:45 -05:00
max pushed to master at max/lean4-htt 2026-05-22 14:10:45 -05:00
ba016b2130 Phase 0: fork infrastructure
ad1c983a43 fix: run beforeElaboration attributes on inductives (#13813)
47e96cd458 feat: add module features to #where command (#13811)
1842bb5476 feat: improve performance of structure instance notation elaboration (#13760)
ed790e99b0 fix: strip hypothesis-naming metadata from proof-mode targets (#13812)
Compare 10 commits »
max created repository max/lean4-htt 2026-05-22 13:31:52 -05:00
max created branch master in max/crosslang 2026-05-12 04:03:02 -05:00
max pushed to master at max/crosslang 2026-05-12 04:03:02 -05:00
4bf2dd38cd Add 'common-lean/' from commit 'a0b719e170f66a736093d0d1c51b9d5883471db2'
bd2e14214d Add 'tsm-lean/' from commit '2e9061abead6f2daa464b39a79c17a949db30785'
6592cd058d Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13'
fd3d42ae33 Add 'golang-lean/' from commit 'f5f17019224c6a6c319387214ceb8e29d09251c6'
6487c7046f Initial commit: crosslang monorepo skeleton.
Compare 10 commits »
max created repository max/crosslang 2026-05-12 04:02:56 -05:00
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 07:32:42 -05:00
391a048dcf Layer 3.3a: substantive unit/counit + typed-correctness for adjoint triple
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 06:07:52 -05:00
0a7228a8e5 Axiom debt cleanup: discharge or convert all 99 engine axioms
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 03:25:12 -05:00
567d8722d5 Refactor Phase 4: Rust ABI v6 → v7 (modal tag unification)
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 03:13:17 -05:00
cfabca3404 Refactor Phase 3a: Modal.lean rewrite — forModalityKind unification
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 03:01:54 -05:00
6e4936d6ee Refactor Phase 2: modal unification — Lean engine cascade
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 02:43:02 -05:00
c334bf9784 Remove Test/Reify.lean — Phase 1 macro-debugging scratch
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 02:42:35 -05:00
2417ec667b Refactor Phase 1: derive_reflect_reify macro — Reflect.lean elegance pass
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 00:28:02 -05:00
c7f91fa933 Modal cascade Phase 3: Modal.lean module proper — Layer 0 complete
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-06 00:18:35 -05:00
c6bc0aa68f Modal cascade Phase 2: Rust ABI v5 → v6 (modal constructors)
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-05 23:22:05 -05:00
b9ca1d8875 Modal cascade Phase 1: Syntax + Lean engine cascade