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 merged pull request aniva/Pantograph#139 2024-12-11 01:13:15 -08:00
fix: Tactic failure on synthesizing placeholder
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-11 01:08:53 -08:00
4217dbcf80 Merge branch 'dev' into bug/tactic-failure-placeholder
c96df2ed1c chore: Add `aarch64` build targets to flake
e9cbc6eab3 chore: Update version
Compare 3 commits »
aniva commented on pull request aniva/Pantograph#139 2024-12-11 00:49:13 -08:00
fix: Tactic failure on synthesizing placeholder

Fixed some more problems. Two test cases in Mathlib:

To reproduce, use these files and pipe them into pantograph-repl's stdin.

frontend.process {"file": "theorem amc12a_2021_p12 (a b c…
aniva deleted branch chore/flake from aniva/Pantograph 2024-12-11 00:30:21 -08:00
aniva pushed to dev at aniva/Pantograph 2024-12-11 00:30:20 -08:00
c96df2ed1c chore: Add `aarch64` build targets to flake
aniva merged pull request aniva/Pantograph#143 2024-12-11 00:30:19 -08:00
chore: Add `aarch64` build targets to flake
aniva created pull request aniva/Pantograph#143 2024-12-11 00:29:56 -08:00
chore: Add aarch64 build targets to flake
aniva created branch chore/flake in aniva/Pantograph 2024-12-11 00:29:41 -08:00
aniva pushed to chore/flake at aniva/Pantograph 2024-12-11 00:29:41 -08:00
c96df2ed1c chore: Add `aarch64` build targets to flake
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-11 00:25:04 -08:00
aa122b2bb9 doc: Update rationale link
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-11 00:21:37 -08:00
58956d33fe doc: Update behaviour rationale
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-11 00:17:07 -08:00
cb87fcd9dd fix: Insert `mvarDeps`
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-10 23:51:53 -08:00
e0e5c9ec68 chore: Code cleanup
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-10 23:49:48 -08:00
755ba13c1b fix: Set `synthesizeSyntheticMVarsNoPostponing`
aniva pushed to bug/tactic-failure-placeholder at aniva/Pantograph 2024-12-10 23:16:56 -08:00
1d10cd2b20 fix: Collect errored mvars by iterating errorInfo
aniva opened issue aniva/Pantograph#142 2024-12-10 21:48:42 -08:00
Pickle new constants generated in proof state
aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-10 21:46:14 -08:00
95503c45e4 doc: frontend.process newConstants
aniva pushed to component/navbar at aniva/Chrysoblog 2024-12-10 18:26:16 -08:00
46ca660a13 merge: branch 'main' into component/navbar
5dbb8e7a8c doc: Documentation about metadata.json
7b900c2993 feat: Read highlighter languages from metadata
0d87cea96f feat: Add more icons
Compare 4 commits »
aniva created pull request aniva/Pantograph#141 2024-12-10 14:15:56 -08:00
feat: Print value of arbitrary mvar in goal state
aniva pushed to goal/print at aniva/Pantograph 2024-12-10 14:15:23 -08:00
0725d865de feat: Print value of arbitrary mvar in goal state