Leni Aniva aniva
  • Stanford University Centaur Group
  • https://leni.sh
  • Admin of this website

  • Joined on 2023-08-21
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
aniva created pull request aniva/Pantograph#86 2024-07-06 19:59:56 -07:00
chore: Update Lean to v4.10.0-rc1
aniva pushed to tactic/eval at aniva/Pantograph 2024-06-27 11:51:29 -07:00
6ddde2963d test: Eval instantiate
aniva pushed to tactic/eval at aniva/Pantograph 2024-06-27 11:34:45 -07:00
fc0d872343 refactor: Simplify proof test infrastructure
aniva created pull request aniva/Pantograph#85 2024-06-26 06:34:27 -07:00
feat: Condensed interface
aniva pushed to tactic/eval at aniva/Pantograph 2024-06-26 04:53:00 -07:00
2d2ff24017 feat: FFI interface for `evaluate` tactic
7acf1ffdf1 refactor: Move `have` to prograde tactic
58f9d72288 test: Evaluate tactic context
c0124b347f Merge branch 'serial/expr' into tactic/eval
8e78718447 feat: Extract MetaM context and state from goal
Compare 12 commits »
aniva opened issue aniva/Pantograph#84 2024-06-25 08:13:36 -07:00
Move towards Expr based interface
aniva created pull request aniva/Pantograph#83 2024-06-23 15:03:30 -07:00
feat: Prograde tactics
aniva pushed to tactic/eval at aniva/Pantograph 2024-06-23 15:02:09 -07:00
25a7025c25 feat: Evaluation tactic
aniva created branch tactic/eval in aniva/Pantograph 2024-06-23 15:02:09 -07:00