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 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
aniva deleted branch tactic/congruence from aniva/Pantograph 2024-06-23 13:35:38 -07:00
aniva pushed to dev at aniva/Pantograph 2024-06-23 13:35:38 -07:00
472cd54868 Merge pull request 'refactor: Cleanup the congruence tactics' (#81) from tactic/congruence into dev
fbe6e8fcb3 Merge branch 'dev' into tactic/congruence
aceee85b05 Merge branch 'env/inspect' into tactic/congruence
f80d90ce87 fix: Goal diag missing newline character
b3a60fcea8 refactor: Rename TacticExecute to SyntheticTactic
Compare 5 commits »
aniva merged pull request aniva/Pantograph#81 2024-06-23 13:35:36 -07:00
refactor: Cleanup the congruence tactics
aniva pushed to tactic/congruence at aniva/Pantograph 2024-06-23 13:35:17 -07:00
fbe6e8fcb3 Merge branch 'dev' into tactic/congruence
361e2e8926 Merge pull request 'fix: aux lemmas in env inspect' (#82) from env/inspect into dev
Compare 2 commits »
aniva closed issue aniva/Pantograph#77 2024-06-23 13:34:03 -07:00
Unclear error message
aniva closed pull request aniva/Pantograph#79 2024-06-23 13:33:55 -07:00
feat: Handling of universe level names in elab
aniva deleted branch env/inspect from aniva/Pantograph 2024-06-23 13:33:38 -07:00
aniva pushed to dev at aniva/Pantograph 2024-06-23 13:33:37 -07:00
361e2e8926 Merge pull request 'fix: aux lemmas in env inspect' (#82) from env/inspect into dev
8707dbc9bb fix: aux lemmas in env inspect
Compare 2 commits »
aniva merged pull request aniva/Pantograph#82 2024-06-23 13:33:35 -07:00
fix: aux lemmas in env inspect
aniva pushed to tactic/congruence at aniva/Pantograph 2024-06-16 13:46:23 -07:00
aceee85b05 Merge branch 'env/inspect' into tactic/congruence
8707dbc9bb fix: aux lemmas in env inspect
Compare 2 commits »
aniva created pull request aniva/Pantograph#82 2024-06-16 13:46:02 -07:00
fix: aux lemmas in env inspect