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 pushed to shell at aniva/config 2024-05-10 11:10:07 -07:00
80b5a2a3d6 fix: Use prompt_hostname instead of hostname
aniva created branch shell in aniva/config 2024-05-10 11:10:07 -07:00
aniva pushed to emacs at aniva/config 2024-05-10 11:08:58 -07:00
c7da83d36e Emacs shell compatibility and SCAD mode
aniva created branch emacs in aniva/config 2024-05-10 11:08:58 -07:00
aniva pushed to linux-sway at aniva/config 2024-05-09 22:37:44 -07:00
354705d709 fix: Screenshot and transparency
aniva created branch linux-sway in aniva/config 2024-05-09 22:37:44 -07:00
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-09 14:03:06 -07:00
0b88f6708e test: Delayed mvar assignment for mapply
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-08 20:51:50 -07:00
e58dbc66a9 fix: Consistent naming in library functions
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-08 12:41:44 -07:00
66a5dfcf3c feat: Diagnostics command for FFI users
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-06 22:39:33 -07:00
69ec70ffbe feat: Do not explicitly show delay assigned mvar
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-06 22:20:46 -07:00
aa106f7591 feat: Do not filter mvars from mapply
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-05 13:26:55 -07:00
679871cbc6 fix: NoConfuse arg name
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-05 13:26:02 -07:00
2937675044 feat: Library interface for calling no_confuse
cf1289f159 feat: NoConfuse tactic
Compare 2 commits »
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-05 10:37:04 -07:00
1e1995255a test: mapply captures dependent types
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-05 00:43:51 -07:00
63417ef179 fix: Motive extra arguments not instiantiated
aniva pushed to goal/mapply at aniva/Pantograph 2024-05-04 23:37:14 -07:00
4cff6677d2 chore: Lean version bump to 4.8.0-rc1
aniva pushed to goal/mapply at aniva/Pantograph 2024-04-22 10:02:27 -07:00
6ffb227cd6 feat: Conduit modus ponens
feff62a3c5 fix: Remove determination of major
Compare 2 commits »
aniva commented on pull request aniva/Pantograph#72 2024-04-22 00:25:03 -07:00
feat: Elementarized tactics with motives, congruence, and absurdity

I think the metavariables generated by mapply don't have to be syntheticOpaque, since no isDefEq operation is contained in it, but we'll see if this is a problem.

aniva opened issue aniva/Pantograph#74 2024-04-22 00:19:29 -07:00
Enable direct expression evaluation in context
aniva pushed to goal/mapply at aniva/Pantograph 2024-04-22 00:12:07 -07:00
3812aa56ec feat: Phantom var in mapply