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-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
aniva deleted branch desktop/waybar from aniva/config 2024-04-20 23:15:14 -07:00
aniva deleted branch desktop/sway from aniva/config 2024-04-20 23:15:13 -07:00
aniva deleted branch macOS from aniva/config 2024-04-20 23:14:42 -07:00
aniva deleted branch emacs from aniva/config 2024-04-20 23:14:35 -07:00
aniva pushed to goal/mapply at aniva/Pantograph 2024-04-20 13:10:14 -07:00
4a92e655f6 test: Tactic test stub
aniva pushed to goal/mapply at aniva/Pantograph 2024-04-19 12:37:42 -07:00
398b1c39ed refactor: Common tactic execute function
fec13ddb51 chore: Code cleanup
Compare 2 commits »
aniva pushed to game/touhou at aniva/OpenMusicScores 2024-04-16 21:43:04 -07:00
6ae0f9ca59 Merge pull request 'Fix Farewell of Slavianka tempo and midi gen' (#7) from march/farewell-of-slavianka into main
ec1bc08c30 Fix Farewell of Slavianka tempo and midi gen
77027c01e9 Merge pull request 'Some English anthems' (#1) from anthems/english into main
515fd0b02e Merge pull request 'Necrofantasia finger positions, Broken Moon' (#3) from game/touhou into main
a651cf228e Merge branch 'main' into anthems/english
Compare 13 commits »
aniva pushed to misc/lemon at aniva/OpenMusicScores 2024-04-16 21:42:47 -07:00
60b3ed9de6 Lemon finger position fix
aniva commented on pull request aniva/Pantograph#72 2024-04-16 15:37:57 -07:00
feat: Elementarized tactics with motives, congruence, and absurdity

MWE to reproduce the implicit lambda problem:

import Lean
open Lean

def parseTerm (s: String): CoreM Syntax := do
  match Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
…
aniva pushed to doc/readme at aniva/Pantograph 2024-04-15 20:01:12 -07:00
7531ad628c doc: Documentation about conditional arguments
aniva created pull request aniva/Pantograph#73 2024-04-15 19:57:39 -07:00
doc: README.md fix