Leni Aniva aniva
  • Stanford University Centaur Lab
  • https://leni.sh
  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-17 16:48:02 -07:00
3733c10a4e refactor: Unify call convention
aniva commented on pull request aniva/Pantograph#83 2024-08-17 02:10:31 -07:00
feat: Prograde tactics

Fixed one of the old glaring bugs of the let tactic where the binder was not introduced. Fixed flake build failure.

Waiting for downstream testing in Trillium before merging.

aniva pushed to tactic/eval at aniva/Pantograph 2024-08-17 02:07:26 -07:00
5d43068ec3 fix: Flake check failure
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-17 02:00:25 -07:00
f87eed817f build: Move non-package output to legacyPackages
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-17 00:53:48 -07:00
43e11f1ba3 refactor: Always display isInaccessible
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-17 00:50:23 -07:00
0c469027c6 fix: Refactor mvar collection in assign tactic
e1b7eaab12 fix: Let tactic not bringing binder into scope
Compare 2 commits »
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-16 00:33:05 -07:00
d17b21e282 fix: Use `getMVarsNoDelayed`
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-15 23:41:43 -07:00
5b4f8a37eb refactor: All Tactic/ tactics into MetaM form
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-15 23:23:32 -07:00
1e7a186bb1 refactor: MetaM form of define (evaluate)
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-15 23:17:44 -07:00
9b0456a5e0 refactor: MetaM form of have and let
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-15 22:54:19 -07:00
7968072097 refactor: Remove the newMVarSet mechanism
aniva pushed to tactic/eval at aniva/Pantograph 2024-08-15 22:45:49 -07:00
e07f9d9b3f Merge branch 'dev' into tactic/eval
56100a30af Merge pull request 'feat: Condensed interface' (#85) from serial/expr into dev
e943a4b065 refactor: Assign into its own tactic
0bc7bc5856 refactor: Remove export of Lean functions
caac70f0cf feat: Move non package outputs to dependencies
Compare 27 commits »
aniva deleted branch serial/expr from aniva/Pantograph 2024-08-15 22:42:00 -07:00
aniva pushed to dev at aniva/Pantograph 2024-08-15 22:42:00 -07:00
56100a30af Merge pull request 'feat: Condensed interface' (#85) from serial/expr into dev
e943a4b065 refactor: Assign into its own tactic
0bc7bc5856 refactor: Remove export of Lean functions
caac70f0cf feat: Move non package outputs to dependencies
64269868d5 feat: Expose project and leanPkgs in flake
Compare 28 commits »
aniva merged pull request aniva/Pantograph#85 2024-08-15 22:41:59 -07:00
feat: Condensed interface
aniva pushed to serial/expr at aniva/Pantograph 2024-08-15 22:40:01 -07:00
e943a4b065 refactor: Assign into its own tactic
aniva pushed to serial/expr at aniva/Pantograph 2024-08-14 01:21:25 -07:00
0bc7bc5856 refactor: Remove export of Lean functions
aniva pushed to serial/expr at aniva/Pantograph 2024-08-04 17:52:57 -07:00
caac70f0cf feat: Move non package outputs to dependencies
aniva pushed to serial/expr at aniva/Pantograph 2024-08-04 17:32:37 -07:00
64269868d5 feat: Expose project and leanPkgs in flake
aniva merged pull request aniva/Pantograph#86 2024-07-06 21:37:31 -07:00
chore: Update Lean to v4.10.0-rc1