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 dev at aniva/Pantograph 2025-05-01 09:26:54 -07:00
06071c1044 Merge pull request 'fix: Shield tactics from the environment generated by `frontend.process`' (#199) from bug/exact-question-mark into dev
f214496c8f Merge branch 'dev' into bug/exact-question-mark
b039018578 Merge branch 'main' into bug/exact-question-mark
49d06e8c05 fix: Shield tactics from newly created environment
170099525c test: Add tactic edge cases test
Compare 6 commits »
aniva deleted branch bug/exact-question-mark from aniva/Pantograph 2025-05-01 09:26:54 -07:00
aniva merged pull request aniva/Pantograph#199 2025-05-01 09:26:53 -07:00
fix: Shield tactics from the environment generated by `frontend.process`
aniva pushed to bug/exact-question-mark at aniva/Pantograph 2025-05-01 09:25:13 -07:00
f214496c8f Merge branch 'dev' into bug/exact-question-mark
0a987174bc Merge pull request 'fix(repl): Elaborate with `errToSorry` as false by default' (#187) from repl/elab-option into dev
eca7431977 Merge pull request 'fix(goal): Prevent duplication in idempotent tactics' (#193) from bug/resume-goal-duplication into dev
c68fed6657 fix(goal): Use `immediateResume` to handle goal
14b74b612d fix(repl): Elaborate with `errToSorry` as false by default
Compare 5 commits »
aniva pushed to bug/exact-question-mark at aniva/Pantograph 2025-05-01 09:24:54 -07:00
b039018578 Merge branch 'main' into bug/exact-question-mark
4e44b147e0 Merge pull request 'chore: Version 0.3' (#136) from dev into main
Compare 2 commits »
aniva pushed to bug/exact-question-mark at aniva/Pantograph 2025-05-01 09:21:52 -07:00
49d06e8c05 fix: Shield tactics from newly created environment
aniva pushed to dev at aniva/Pantograph 2025-05-01 09:00:05 -07:00
0a987174bc Merge pull request 'fix(repl): Elaborate with `errToSorry` as false by default' (#187) from repl/elab-option into dev
14b74b612d fix(repl): Elaborate with `errToSorry` as false by default
Compare 2 commits »
aniva merged pull request aniva/Pantograph#187 2025-05-01 09:00:04 -07:00
fix(repl): Elaborate with `errToSorry` as false by default
aniva pushed to dev at aniva/Pantograph 2025-05-01 08:59:38 -07:00
eca7431977 Merge pull request 'fix(goal): Prevent duplication in idempotent tactics' (#193) from bug/resume-goal-duplication into dev
c68fed6657 fix(goal): Use `immediateResume` to handle goal
Compare 2 commits »
aniva deleted branch bug/resume-goal-duplication from aniva/Pantograph 2025-05-01 08:59:38 -07:00
aniva closed issue aniva/Pantograph#192 2025-05-01 08:59:37 -07:00
Goal duplication
aniva merged pull request aniva/Pantograph#193 2025-05-01 08:59:37 -07:00
fix(goal): Prevent duplication in idempotent tactics
aniva created pull request aniva/Pantograph#199 2025-05-01 08:59:16 -07:00
fix: Shield tactics from the environment generated by frontend.process
aniva created branch bug/exact-question-mark in aniva/Pantograph 2025-05-01 08:10:11 -07:00
aniva pushed to bug/exact-question-mark at aniva/Pantograph 2025-05-01 08:10:11 -07:00
170099525c test: Add tactic edge cases test
aniva opened issue aniva/Pantograph#198 2025-04-27 10:04:57 -07:00
Add documentation about what we cannot implement
aniva commented on issue aniva/Pantograph#151 2025-04-25 08:21:40 -07:00
Add unsafe detection in goal.print

We should also output messages after a tactic to service things such as trace_state.

After each tactic, we can report whether the proof expression created in the mvars and delayed mvars have…

aniva opened issue aniva/Pantograph#197 2025-04-24 08:45:23 -07:00
Condition Unification
aniva opened issue aniva/Pantograph#196 2025-04-23 05:50:17 -07:00
Documentation about safety
aniva pushed to touhou/yasaka-kanako at aniva/Cosplay 2025-04-22 11:17:01 -07:00
7511efa9ee Add Kanako set class