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
12
 Projects Packages Public Activity Starred Repositories
9
aniva pushed to dev at aniva/Pantograph 2024-08-31 20:04:40 -07:00
948b535b5d Merge pull request 'feat: Prograde tactics' (#83) from tactic/eval into dev
edec0f5733 feat: Use CoreM for diag monad
0c529c5cd9 Merge branch 'misc/test-driver' into tactic/eval
3733c10a4e refactor: Unify call convention
5d43068ec3 fix: Flake check failure
Compare 25 commits »
aniva merged pull request aniva/Pantograph#83 2024-08-31 20:04:39 -07:00
feat: Prograde tactics
aniva opened issue aniva/Pantograph#88 2024-08-31 19:57:41 -07:00
Resumption not taking into account type unification
aniva closed issue aniva/Pantograph#74 2024-08-31 19:54:12 -07:00
Enable direct expression evaluation in context
aniva commented on issue aniva/Pantograph#74 2024-08-31 19:54:12 -07:00
Enable direct expression evaluation in context

Exposed interface for MetaM context and state in #85.

aniva closed issue aniva/Pantograph#67 2024-08-31 19:53:35 -07:00
Extraction of atomization step
aniva commented on issue aniva/Pantograph#67 2024-08-31 19:53:34 -07:00
Extraction of atomization step

Atomization is too tightly coupled to the user architecture. We'll not include it here in the forseeable future. Vide aniva/Trillium#124: A new Catenary library was…

aniva closed issue aniva/Pantograph#80 2024-08-31 19:51:43 -07:00
Expose the String.toName interface
aniva commented on issue aniva/Pantograph#80 2024-08-31 19:51:43 -07:00
Expose the String.toName interface

The user should call into Lean's kernel directly for this kind of features. We'll not re-expose functions in the Lean kernel.

aniva commented on issue aniva/Pantograph#84 2024-08-31 19:50:54 -07:00
Move towards Expr based interface

Done #85

aniva closed issue aniva/Pantograph#84 2024-08-31 19:50:54 -07:00
Move towards Expr based interface
aniva pushed to main at aniva/ReproduciblePython 2024-08-27 22:32:11 -07:00
f2916e1785 feat: Add torch stub
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-26 10:42:35 -07:00
edec0f5733 feat: Use CoreM for diag monad
aniva deleted branch misc/test-driver from aniva/Pantograph 2024-08-18 12:24:57 -07:00
aniva pushed to dev at aniva/Pantograph 2024-08-18 12:24:56 -07:00
76765c913c test: Use `lake test`. Retired `Makefile`
aniva merged pull request aniva/Pantograph#87 2024-08-18 12:24:56 -07:00
test: Use `lake test`. Retired `Makefile`
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-18 12:24:51 -07:00
0c529c5cd9 Merge branch 'misc/test-driver' into tactic/eval
76765c913c test: Use `lake test`. Retired `Makefile`
Compare 2 commits »
aniva created pull request aniva/Pantograph#87 2024-08-18 12:23:54 -07:00
test: Use lake test. Retired Makefile
aniva pushed to misc/test-driver at aniva/Pantograph 2024-08-18 12:23:24 -07:00
76765c913c test: Use `lake test`. Retired `Makefile`
aniva created branch misc/test-driver in aniva/Pantograph 2024-08-18 12:23:24 -07:00