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 closed pull request aniva/Pantograph#89 2024-09-02 19:43:36 -07:00

fix: Resume not taking type unification into account

aniva commented on pull request aniva/Pantograph#89 2024-09-02 19:43:36 -07:00

fix: Resume not taking type unification into account

The bug is not due to this repo

aniva commented on issue aniva/Pantograph#88 2024-09-02 19:43:22 -07:00

Resumption not taking type unification into account

This was a bug in the downstream Tactic.exact implementation.

aniva closed issue aniva/Pantograph#88 2024-09-02 19:43:22 -07:00

Resumption not taking type unification into account

aniva opened issue aniva/config#13 2024-09-02 17:33:07 -07:00

Emacs freezes while using LSP

aniva closed issue aniva/config#6 2024-09-02 17:31:39 -07:00

Replace waybar with eww

aniva commented on issue aniva/config#6 2024-09-02 17:31:39 -07:00

Replace waybar with eww

Done

aniva created pull request aniva/Pantograph#89 2024-08-31 20:08:36 -07:00

fix: Resume not taking type unification into account

aniva pushed to bug/resume-type-unification at aniva/Pantograph 2024-08-31 20:08:04 -07:00

aniva created branch bug/resume-type-unification in aniva/Pantograph 2024-08-31 20:08:04 -07:00

aniva deleted branch tactic/eval from aniva/Pantograph 2024-08-31 20:04:40 -07:00

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 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#74 2024-08-31 19:54:12 -07:00

Enable direct expression evaluation in context

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.