fix tests

leanprover · Dec 15, 2024 · 3b355db · 3b355db
1 parent 4e95e5c
commit 3b355db
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/tests/lean/getElem.lean b/tests/lean/getElem.lean
@@ -45,7 +45,7 @@ def withTwoRanges (xs : Array Nat) : Option Nat := Id.run do
 
 def palindromeNeedsOmega (xs : Array Nat) : Bool := Id.run do
   for h : i in [:xs.size/2] do
-    have : i < xs.size/2 := h.2 -- omega does not understand range yet
+    have : i < xs.size/2 := h.2.1 -- omega does not understand range yet
     if xs[xs.size - 1 - i] ≠ xs[i] then
       return false
   return true
diff --git a/tests/lean/run/structure_recursive.lean b/tests/lean/run/structure_recursive.lean
@@ -95,7 +95,7 @@ def Foo'.preorder : Foo' → String
   | {name, n, children} => Id.run do
     let mut acc := name
     for h : i in [0:n] do
-      acc := acc ++ (children ⟨i, h.2⟩).preorder
+      acc := acc ++ (children ⟨i, h.2.1⟩).preorder
     return acc
 
 /-- info: Foo'.preorder : Foo' → String -/