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
13
 Projects Packages Public Activity Starred Repositories
9
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
aniva created branch doc/readme in aniva/Pantograph 2024-04-15 19:57:21 -07:00
aniva pushed to doc/readme at aniva/Pantograph 2024-04-15 19:57:21 -07:00
52e5b5df50 doc: README.md fix
aniva commented on pull request aniva/Pantograph#72 2024-04-15 13:03:31 -07:00
feat: Elementarized tactics with motives, congruence, and absurdity

Waiting for this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Elaborator.20and.20.40/near/433364676

aniva deleted branch lib/mkOptions from aniva/Pantograph 2024-04-15 12:58:10 -07:00
aniva pushed to dev at aniva/Pantograph 2024-04-15 12:58:09 -07:00
adbb07af2d fix: Option setting in REPL
aniva merged pull request aniva/Pantograph#71 2024-04-15 12:58:08 -07:00
fix: Option setting in REPL