diff --git a/tests/lean/run/998.lean b/tests/lean/run/998.lean new file mode 100644 index 0000000000..cf61f27a52 --- /dev/null +++ b/tests/lean/run/998.lean @@ -0,0 +1,13 @@ +import Lean +set_option maxHeartbeats 100000 +-- attribute [simp] Array.findIdx?.loop -- Still broken +attribute [simp] Lean.expandExplicitBindersAux.loop +attribute [simp] Lean.Elab.Term.resolveLocalName.loop + + +-- Mathlib +-- attribute [simp] BinaryHeap.heapifyDown +-- attribute [simp] ByteSlice.forIn.loop +-- attribute [simp] Lean.Export.exportName +-- attribute [simp] Lean.Export.exportLevel +-- attribute [simp] Array.heapSort.loop