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
13
 Projects Packages Public Activity Starred Repositories
9
aniva merged pull request aniva/Pantograph#128 2024-12-11 01:25:36 -08:00
feat: Extract type error and new constants
aniva closed issue aniva/Pantograph#122 2024-12-11 01:25:36 -08:00
Mathlib4 Parsing Error
aniva commented on issue aniva/Pantograph#102 2024-12-11 01:16:38 -08:00
Timeout for tactics

https://github.com/leanprover/lean4/issues/3812

aniva pushed to frontend/infotree at aniva/Pantograph 2024-12-11 01:14:49 -08:00
7cba8efd54 Merge branch 'dev' into frontend/infotree
e9fbce7b4d Merge pull request 'fix: Tactic failure on synthesizing placeholder' (#139) from bug/tactic-failure-placeholder into dev
4217dbcf80 Merge branch 'dev' into bug/tactic-failure-placeholder
c96df2ed1c chore: Add `aarch64` build targets to flake
aa122b2bb9 doc: Update rationale link
Compare 14 commits »
aniva deleted branch bug/tactic-failure-placeholder from aniva/Pantograph 2024-12-11 01:13:17 -08:00
aniva pushed to dev at aniva/Pantograph 2024-12-11 01:13:16 -08:00
e9fbce7b4d Merge pull request 'fix: Tactic failure on synthesizing placeholder' (#139) from bug/tactic-failure-placeholder into dev
4217dbcf80 Merge branch 'dev' into bug/tactic-failure-placeholder
aa122b2bb9 doc: Update rationale link
58956d33fe doc: Update behaviour rationale
cb87fcd9dd fix: Insert `mvarDeps`
Compare 11 commits »
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 pushed to chore/flake at aniva/Pantograph 2024-12-11 00:29:41 -08:00
c96df2ed1c 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 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`