From 96336bb44d8db2397ba2e552f64b92f45c69b6a1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Feb 2022 11:41:24 -0800 Subject: [PATCH] test: add tests for #998 The previous changes fixed two of them. --- tests/lean/run/998.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 tests/lean/run/998.lean 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