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 created pull request aniva/config#21 2024-10-03 17:27:21 -07:00
feat: Use two line fish prompt
aniva pushed to ui/fish at aniva/config 2024-10-03 17:27:04 -07:00
1c49965dcb feat: Use two line fish prompt
aniva created branch ui/fish in aniva/config 2024-10-03 17:27:04 -07:00
aniva deleted branch shell from aniva/config 2024-10-03 17:15:31 -07:00
aniva pushed to main at aniva/config 2024-10-03 17:09:50 -07:00
c130537892 Merge pull request 'feat: Kando' (#20) from ui/kando into main
274d09ce54 feat: macOS keybindings
0c51670191 feat: Basic Kando menu
Compare 3 commits »
aniva merged pull request aniva/config#20 2024-10-03 17:09:48 -07:00
feat: Kando
aniva created pull request aniva/config#20 2024-10-03 17:09:20 -07:00
feat: Kando
aniva opened issue aniva/Pantograph#104 2024-10-03 15:49:01 -07:00
goal.delete exceeds max recursion depth
aniva commented on issue aniva/Pantograph#97 2024-10-03 15:43:31 -07:00
Parse and enter environment at arbitrary points of the input

Done #99

aniva closed issue aniva/Pantograph#97 2024-10-03 15:43:31 -07:00
Parse and enter environment at arbitrary points of the input
aniva deleted branch frontend/collect-holes from aniva/Pantograph 2024-10-03 15:43:02 -07:00
aniva pushed to dev at aniva/Pantograph 2024-10-03 15:43:02 -07:00
452c390711 Merge pull request 'feat: Collect holes in Lean file and put them into a `GoalState`' (#99) from frontend/collect-holes into dev
10cb32e03f Merge branch 'dev' into frontend/collect-holes
a03eeddc9b fix: Variable duplication in nested translation
530a1a1a97 fix: Extracting `sorry`s from coupled goals
143cd289bb fix: Extraction of sorry's from nested tactics
Compare 15 commits »
aniva merged pull request aniva/Pantograph#99 2024-10-03 15:43:01 -07:00
feat: Collect holes in Lean file and put them into a `GoalState`
aniva commented on issue aniva/Pantograph#103 2024-10-03 11:51:44 -07:00
Metavariable not found bug with sorry collection

Fixed

aniva closed issue aniva/Pantograph#103 2024-10-03 11:51:44 -07:00
Metavariable not found bug with sorry collection
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-10-03 11:47:42 -07:00
10cb32e03f Merge branch 'dev' into frontend/collect-holes
b174b4ea79 Merge pull request 'fix: Tactics should produce `.syntheticOpaque` goals' (#100) from goal/tactic into dev
ed1f96d7f7 Merge branch 'dev' into goal/tactic
5e99237e09 fix: Tactics should produce `.syntheticOpaque` goals
Compare 4 commits »
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-10-03 11:46:27 -07:00
a03eeddc9b fix: Variable duplication in nested translation
aniva commented on pull request aniva/Pantograph#99 2024-10-03 11:38:21 -07:00
feat: Collect holes in Lean file and put them into a GoalState

Currently there's a variable duplication issue in coupled goals:

def test_sorry_in_coupled: TestT MetaM Unit := do
  let sketch := "
example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x :=…
aniva pushed to frontend/collect-holes at aniva/Pantograph 2024-10-03 11:36:18 -07:00
530a1a1a97 fix: Extracting `sorry`s from coupled goals
aniva pushed to dev at aniva/Pantograph 2024-10-03 08:47:32 -07:00
b174b4ea79 Merge pull request 'fix: Tactics should produce `.syntheticOpaque` goals' (#100) from goal/tactic into dev
ed1f96d7f7 Merge branch 'dev' into goal/tactic
5e99237e09 fix: Tactics should produce `.syntheticOpaque` goals
Compare 3 commits »