Leni Aniva aniva
0 Followers · 1 Following
  • Stanford University Centaur Group
  • https://leni.sh

  • Admin of this website

  • Joined on 2023-08-21
Repositories
10
 Projects Packages Public Activity Starred Repositories
2
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 created branch misc/version in aniva/Pantograph 2024-05-17 20:32:02 -07:00
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 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…
aniva pushed to linux-sway at aniva/config 2024-05-10 20:48:57 -07:00
46f3f1fffe fix: Screenshot and transparency
301b57ec06 Initial commit
Compare 2 commits »
aniva pushed to shell at aniva/config 2024-05-10 20:48:22 -07:00
53f3c5d63d fix: Use prompt_hostname instead of hostname
301b57ec06 Initial commit
Compare 2 commits »
aniva pushed to main at aniva/config 2024-05-10 20:47:25 -07:00
301b57ec06 Initial commit
aniva pushed to emacs at aniva/config 2024-05-10 20:47:08 -07:00
4ff5cfd3f9 feat: Emacs shell compatibility and SCAD mode
aniva commented on pull request aniva/Pantograph#72 2024-05-10 14:38:38 -07:00
feat: Elementarized tactics with motives, congruence, and absurdity

This breaks current metavariable resolution schema because the motive variable is delay assigned. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Force.20instantiate.20delay.…

aniva created pull request aniva/config#12 2024-05-10 14:31:12 -07:00
fix: Linux sway and eww settings
aniva created pull request aniva/config#11 2024-05-10 14:30:25 -07:00
fix: Fish shell fix
aniva created pull request aniva/config#10 2024-05-10 11:11:06 -07:00
feat: Emacs shell compatibility and SCAD mode
aniva pushed to emacs at aniva/config 2024-05-10 11:10:16 -07:00
9a4a987d64 feat: Emacs shell compatibility and SCAD mode