update for GetElem

leanprover-community · Jun 25, 2024 · eba621c · eba621c
1 parent 18f2a5d
commit eba621c
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/ProofWidgets/Data/Svg.lean b/ProofWidgets/Data/Svg.lean
@@ -188,9 +188,13 @@ def idToData {f} (svg : Svg f) : HashMap String Json :=
 
 instance {f} : GetElem (Svg f) Nat (Svg.Element f) (λ svg idx => idx < svg.elements.size) where
   getElem svg i h := svg.elements[i]
+  getElem? svg i := svg.elements[i]?
+  getElem! svg i := svg.elements[i]!
 
 instance {f} : GetElem (Svg f) String (Option (Svg.Element f)) (λ _ _ => True) where
   getElem svg id _ := svg.idToIdx[id].map (λ idx => svg.elements[idx])
+  getElem? svg id := svg.idToIdx[id].map (λ idx => svg.elements[idx]?)
+  getElem! svg id := svg.idToIdx[id].map (λ idx => svg.elements[idx])
 
 def getData {f} (svg : Svg f) (id : String) : Option Json :=
   match svg[id] with

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-06-24
+leanprover/lean4-pr-releases:pr-release-4560