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 pushed to goal/mapply at aniva/Pantograph 2024-05-20 11:55:49 -07:00
75df7268c5 test: Simplify testing structure for tactics
92acf7782c test: CongruenceArg tactic
Compare 2 commits »
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-20 11:08:23 -07:00
cf1c884c8c Merge branch 'dev' into goal/mapply
0aec757601 Merge pull request 'doc: README.md fix' (#73) from doc/readme into dev
e05c01109c Merge branch 'dev' into doc/readme
e165e41efa chore: Version bump to v4.8.0-rc1
7531ad628c doc: Documentation about conditional arguments
Compare 7 commits »
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-20 10:56:05 -07:00
cc74d41b15 feat: Congruence tactics
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-19 15:43:58 -07:00
2f951c8fef fix: Decoupling of mvars during instantiation
aniva pushed to dev at aniva/Pantograph 2024-05-17 20:33:20 -07:00
0aec757601 Merge pull request 'doc: README.md fix' (#73) from doc/readme into dev
e05c01109c Merge branch 'dev' into doc/readme
7531ad628c doc: Documentation about conditional arguments
52e5b5df50 doc: README.md fix
Compare 4 commits »
aniva merged pull request aniva/Pantograph#73 2024-05-17 20:33:19 -07:00
doc: README.md fix
aniva pushed to doc/readme at aniva/Pantograph 2024-05-17 20:33:08 -07:00
e05c01109c Merge branch 'dev' into doc/readme
e165e41efa chore: Version bump to v4.8.0-rc1
adbb07af2d fix: Option setting in REPL
Compare 3 commits »
aniva deleted branch misc/version from aniva/Pantograph 2024-05-17 20:32:31 -07:00
aniva pushed to dev at aniva/Pantograph 2024-05-17 20:32:31 -07:00
e165e41efa chore: Version bump to v4.8.0-rc1
aniva merged pull request aniva/Pantograph#75 2024-05-17 20:32:30 -07:00
chore: Version bump to v4.8.0-rc1
aniva created pull request aniva/Pantograph#75 2024-05-17 20:32:21 -07:00
chore: Version bump to v4.8.0-rc1
aniva pushed to misc/version at aniva/Pantograph 2024-05-17 20:32:02 -07:00
e165e41efa chore: Version bump to v4.8.0-rc1
aniva created branch misc/version in aniva/Pantograph 2024-05-17 20:32:02 -07:00
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-16 10:32:01 -07:00
6ad24b72d4 fix: Nested delayed assignment instantiation
cf17428001 fix: Panic in partial instantiation
Compare 2 commits »
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-14 19:33:52 -07:00
5c7bb288b2 feat: Display full free variable list in subst
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-13 13:59:04 -07:00
bc09f4a29d refactor: Expr related functions to Expr.lean
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-13 13:49:35 -07:00
f813d4a8dd refactor: Delayed mvar instantiation function
aniva commented on pull request aniva/Pantograph#72 2024-05-13 12:42:49 -07:00
feat: Elementarized tactics with motives, congruence, and absurdity

I've decided to go with method (3). This requires a new abstraction in the sexp layer. Maybe the sexp should just be removed.

aniva pushed to goal/mapply at aniva/Pantograph 2024-05-12 22:33:52 -07:00
c04b363de7 feat: Handle delay assigned mvars
03ecb6cf19 feat: Partial instantiate metavariables
Compare 2 commits »
aniva commented on pull request aniva/Pantograph#72 2024-05-11 15:37:45 -07:00
feat: Elementarized tactics with motives, congruence, and absurdity

There are currently 3 solutions to this issue:

  1. Add value dependency to the current handling of traces
  2. Use a partial delaboration function like above
  3. When producing sexp, use a similar…