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 deleted branch repl/flush from aniva/Pantograph 2025-04-20 09:29:06 -07:00
aniva pushed to dev at aniva/Pantograph 2025-04-20 09:29:05 -07:00
a2f9d77cb5 Merge pull request 'feat(repl): Flush stdout' (#194) from repl/flush into dev
a88829f9be Merge branch 'dev' into repl/flush
d9c484230b feat(repl): Flush stdout
Compare 3 commits »
aniva merged pull request aniva/Pantograph#194 2025-04-20 09:29:04 -07:00
feat(repl): Flush stdout
aniva pushed to repl/flush at aniva/Pantograph 2025-04-20 09:28:58 -07:00
a88829f9be Merge branch 'dev' into repl/flush
fa5d423005 Merge pull request 'doc: Update rationale' (#189) from doc/rationale into dev
60f79f5f02 doc: Fix typo
4abe2fa72f fix: LEAN_PATH example
77b517f4c6 doc: Update rationale about timeout
Compare 5 commits »
aniva created pull request aniva/Pantograph#194 2025-04-20 09:28:24 -07:00
feat(repl): Flush stdout
aniva pushed to repl/flush at aniva/Pantograph 2025-04-20 09:27:13 -07:00
d9c484230b feat(repl): Flush stdout
aniva created branch repl/flush in aniva/Pantograph 2025-04-20 09:27:13 -07:00
aniva commented on issue aniva/Pantograph#192 2025-04-18 10:10:29 -07:00
Goal duplication

This is a pathological behaviour from Mathlib's ring_nf tactic. We could add a guard for it.

aniva deleted branch doc/rationale from aniva/Pantograph 2025-04-18 01:08:26 -07:00
aniva pushed to dev at aniva/Pantograph 2025-04-18 01:08:26 -07:00
fa5d423005 Merge pull request 'doc: Update rationale' (#189) from doc/rationale into dev
60f79f5f02 doc: Fix typo
4abe2fa72f fix: LEAN_PATH example
77b517f4c6 doc: Update rationale about timeout
Compare 4 commits »
aniva merged pull request aniva/Pantograph#189 2025-04-18 01:08:25 -07:00
doc: Update rationale
aniva created pull request aniva/Pantograph#193 2025-04-18 00:44:11 -07:00
fix(goal): Prevent duplication in idempotent tactics
aniva opened issue aniva/Pantograph#192 2025-04-18 00:24:43 -07:00
Goal duplication
aniva pushed to doc/rationale at aniva/Pantograph 2025-04-14 23:26:37 -07:00
60f79f5f02 doc: Fix typo
aniva commented on issue aniva/Pantograph#191 2025-04-14 16:48:36 -07:00
Code generation of recursors

Also vide: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.E2.9C.94.20.22code.20generator.20does.20not.20support.20recursor.22

This is related to generating recursive…

aniva pushed to doc/rationale at aniva/Pantograph 2025-04-14 16:27:40 -07:00
4abe2fa72f fix: LEAN_PATH example
aniva opened issue aniva/Pantograph#191 2025-04-14 16:23:39 -07:00
Code generation of recursors
aniva commented on issue aniva/Pantograph#190 2025-04-14 16:08:09 -07:00
Use non-computable section by default

Also if we want to generate code, we may need to wait until the code generator can handle recursors. Vide Canonical.

aniva opened issue aniva/Pantograph#190 2025-04-14 16:01:57 -07:00
Use non-computable section by default
aniva pushed tag v0.3.0 to aniva/Pantograph 2025-04-14 15:32:44 -07:00