Skip to content

Commit

Permalink
fix test
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Dec 10, 2024
1 parent 95207f3 commit bdd0c5b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion tests/lean/run/wfOverapplicationIssue.lean
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : as.contains a) : sizeOf a < sizeOf as := by
simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (b = a)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
unfold anyM.loop
intro h
split at h
Expand Down

0 comments on commit bdd0c5b

Please sign in to comment.