Leni Aniva aniva
0 Followers · 1 Following
  • Stanford University Centaur Lab
  • https://leni.sh

  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
Repositories
13
 Projects Packages Public Activity Starred Repositories
9
aniva commented on issue aniva/Pantograph#225 2025-07-01 12:47:59 -07:00
Could not load mathlib environment from saved file

The main problem is this part:

// src/library/compiler/ir_interpreter.cpp

        // no native code, so might be part of the current module
        if (get_regular_init_fn_name_for(m…
aniva opened issue aniva/Pantograph#225 2025-07-01 12:35:21 -07:00
Could not load mathlib environment from saved file
aniva created pull request aniva/Pantograph#224 2025-06-30 15:57:30 -07:00
doc: Remove constraint on pick_goal
aniva pushed to doc/rationale at aniva/Pantograph 2025-06-30 15:57:01 -07:00
50bb48f2ed doc: Remove constraint on pick_goal
aniva created branch doc/rationale in aniva/Pantograph 2025-06-30 15:57:01 -07:00
aniva pushed to dev at aniva/Pantograph 2025-06-30 15:28:29 -07:00
f26b7fc177 Merge pull request 'fix(goal): Unknown metavariable problem during fragment initialization' (#222) from bug/unknown-metavariable-fragment into dev
16474b2ce8 test(repl): Add test for conv and calc
3fab7e7818 fix(repl): Allow .none in parentExpr
dd7c6c36c8 fix(goal): Allow parent expr to be fragments
8857b88d9a fix(goal): Restore elaboration monad
Compare 5 commits »
aniva merged pull request aniva/Pantograph#222 2025-06-30 15:28:29 -07:00
fix(goal): Unknown metavariable problem during fragment initialization
aniva deleted branch bug/unknown-metavariable-fragment from aniva/Pantograph 2025-06-30 15:28:29 -07:00
aniva pushed to bug/unknown-metavariable-fragment at aniva/Pantograph 2025-06-30 15:28:12 -07:00
16474b2ce8 test(repl): Add test for conv and calc
aniva pushed to bug/unknown-metavariable-fragment at aniva/Pantograph 2025-06-30 15:08:58 -07:00
3fab7e7818 fix(repl): Allow .none in parentExpr
aniva created pull request aniva/Pantograph#223 2025-06-30 15:05:33 -07:00
chore: Update Lean to v4.21.0
aniva pushed to chore/toolchain at aniva/Pantograph 2025-06-30 15:05:19 -07:00
7b96652c87 chore: Update Lean to v4.21.0
aniva created branch chore/toolchain in aniva/Pantograph 2025-06-30 15:05:19 -07:00
aniva pushed to bug/unknown-metavariable-fragment at aniva/Pantograph 2025-06-30 15:00:42 -07:00
dd7c6c36c8 fix(goal): Allow parent expr to be fragments
aniva pushed to bug/unknown-metavariable-fragment at aniva/Pantograph 2025-06-30 14:53:03 -07:00
8857b88d9a fix(goal): Restore elaboration monad
aniva created pull request aniva/Pantograph#222 2025-06-30 14:43:31 -07:00
fix(goal): Unknown metavariable problem during fragment initialization
aniva pushed to bug/unknown-metavariable-fragment at aniva/Pantograph 2025-06-30 14:42:44 -07:00
aniva created branch bug/unknown-metavariable-fragment in aniva/Pantograph 2025-06-30 14:42:44 -07:00
aniva created pull request aniva/config#27 2025-06-30 11:02:41 -07:00
chore: Fix indentation problems in emacs
aniva pushed to touhou at aniva/OpenMusicScores 2025-06-29 22:42:24 -07:00
9ff4decabe Add documentation about notation