Leni Aniva aniva
  • Stanford University Centaur Group
  • https://leni.sh
  • Admin of this website

  • Joined on 2023-08-21
Loading Heatmap…

aniva pushed to goal/mapply at aniva/Pantograph

2024-05-20 11:08:23 -07:00

aniva pushed to goal/mapply at aniva/Pantograph

2024-05-20 10:56:05 -07:00

aniva pushed to goal/mapply at aniva/Pantograph

  • 2f951c8fef fix: Decoupling of mvars during instantiation

2024-05-19 15:43:58 -07:00

aniva pushed to dev at aniva/Pantograph

2024-05-17 20:33:20 -07:00

aniva merged pull request aniva/Pantograph#73

doc: README.md fix

2024-05-17 20:33:19 -07:00

aniva pushed to doc/readme at aniva/Pantograph

2024-05-17 20:33:08 -07:00

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

aniva merged pull request aniva/Pantograph#75

chore: Version bump to v4.8.0-rc1

2024-05-17 20:32:30 -07:00

aniva created pull request aniva/Pantograph#75

chore: Version bump to v4.8.0-rc1

2024-05-17 20:32:21 -07:00

aniva pushed to misc/version at aniva/Pantograph

2024-05-17 20:32:02 -07:00

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

aniva pushed to goal/mapply at aniva/Pantograph

  • 5c7bb288b2 feat: Display full free variable list in subst

2024-05-14 19:33:52 -07:00

aniva pushed to goal/mapply at aniva/Pantograph

  • bc09f4a29d refactor: Expr related functions to Expr.lean

2024-05-13 13:59:04 -07:00

aniva pushed to goal/mapply at aniva/Pantograph

  • f813d4a8dd refactor: Delayed mvar instantiation function

2024-05-13 13:49:35 -07:00

aniva commented on pull request aniva/Pantograph#72

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.

2024-05-13 12:42:49 -07:00

aniva pushed to goal/mapply at aniva/Pantograph

2024-05-12 22:33:52 -07:00

aniva commented on pull request aniva/Pantograph#72

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…

2024-05-11 15:37:45 -07:00

aniva pushed to linux-sway at aniva/config

2024-05-10 20:48:57 -07:00