chore: updates for nightly 2024-09-17

.github/workflows/ci.yml

@@ -27,6 +27,7 @@ jobs:
           - "nightly-2024-08-09"
           - "nightly-2024-08-29"
           - "nightly-2024-09-03"
+          - "nightly-2024-09-17"
         platform:
           - os: ubuntu-latest
             installer: |

InternalTests.lean

@@ -73,10 +73,10 @@ elab "#evalString" s:str e:term : command => do
     modify ({· with messages := msgs})
 
 #evalString "[[\"n * 1 = n\"]]\n"
-  (proofEx.highlighted[0].proofStates.data.filter (·.fst == "by") |>.map (·.snd.data.map (·.conclusion)))
+  (proofEx.highlighted[0].proofStates.toList.filter (·.fst == "by") |>.map (·.snd.toList.map (·.conclusion)))
 
 #evalString "[[some `zero], [some `succ], [none], [some `succ.succ], [none]]\n"
-  (proofEx.highlighted[0].proofStates.data.filter (·.fst == "=>") |>.map (·.snd.data.map (·.name)))
+  (proofEx.highlighted[0].proofStates.toList.filter (·.fst == "=>") |>.map (·.snd.toList.map (·.name)))
 
 
 

src/highlighting/SubVerso/Highlighting/Code.lean

@@ -87,14 +87,26 @@ def insert [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (x : α) :
     }
     pure i
 
-partial def find [Inhabited α] [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (x : α) : m (Nat × α × Nat) := do
-  loop <| ← insert x
-where
-  loop (i : Nat) : m (Nat × α × Nat) := do
-    match (← get).contents[i]! with
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
+  h1.elim fun x =>
+    h2.elim fun y =>
+      ⟨(x, y)⟩
+
+
+example [Inhabited α] [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (x : α) : Inhabited (m (Nat × α × Nat)) := inferInstance
+
+-- Lifted from find's where block to make sure the Inhabited instance is found
+partial def find.loop [Inhabited α] [Monad m] [MonadState (State α) m] (i : Nat) : m (Nat × α × Nat) := do
+    -- Instance needed in Lean 4.12 and onwards, where there's Nonempty but not Inhabited instances
+    -- for Sum
+    let _ : Inhabited (Nat ⊕ α × Nat) := ⟨.inl default⟩
+    match (← get).contents[i]?.get! with
     | .inl j => loop j
     | .inr (v, sz) => return (i, v, sz)
 
+def find [Inhabited α] [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (x : α) : m (Nat × α × Nat) := do
+  find.loop <| ← insert x
+
 def equate [Inhabited α] [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (x y : α) : m Unit := do
   let mut x' ← find x
   let mut y' ← find y