max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: add tests for #998

Browse source 
The previous changes fixed two of them.
This commit is contained in:
Leonardo de Moura 2022-02-08 11:41:24 -08:00
parent c486203481
commit 96336bb44d
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
tests/lean/run/998.lean Normal file
View file

@ -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