- Stanford University Centaur Group
- https://leni.sh
-
Admin of this website
- Joined on
2023-08-21
398b1c39ed
refactor: Common tactic execute function
fec13ddb51
chore: Code cleanup
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
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)
…
fix: Option setting in REPL