From a4b3b0013b221714d4e9c947cfe850a3408f60fb Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 7 Mar 2024 19:56:43 +0000 Subject: [PATCH 1/2] fix(slim_check): do not crash when binders contain a function type --- Mathlib/Testing/SlimCheck/Testable.lean | 2 +- test/slim_check.lean | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/Mathlib/Testing/SlimCheck/Testable.lean b/Mathlib/Testing/SlimCheck/Testable.lean index 3d515028a2d32..2b5c1340f68ea 100644 --- a/Mathlib/Testing/SlimCheck/Testable.lean +++ b/Mathlib/Testing/SlimCheck/Testable.lean @@ -509,7 +509,7 @@ open Lean quantifiers and add `NamedBinder` annotations next to them. -/ partial def addDecorations (e : Expr) : MetaM Expr := Meta.transform e fun expr => do - if not (← Meta.inferType e).isProp then + if not (← Meta.inferType expr).isProp then return .continue else if let Expr.forallE name type body data := expr then let newType ← addDecorations type diff --git a/test/slim_check.lean b/test/slim_check.lean index 00665c858bc2a..5c122154fa362 100644 --- a/test/slim_check.lean +++ b/test/slim_check.lean @@ -413,6 +413,21 @@ issue: ⋯ does not hold exact test_sorry trivial +open scoped BigOperators in +example (n : ℕ) : true := by + have : ∑ f : Unit → Fin (n + 1), f () = 0 := by + success_if_fail_with_msg " +=================== +Found problems! +n := 1 +issue: 1 = 0 does not hold +(0 shrinks) +------------------- +" + slim_check (config := { randomSeed := some 257 }) + exact test_sorry + trivial + -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slim_check.20question/near/412709012 open scoped BigOperators in /-- From 0c47666f17acec611f48c54675737510b0167918 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 7 Mar 2024 20:23:43 +0000 Subject: [PATCH 2/2] fix recursion --- Mathlib/Testing/SlimCheck/Testable.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Testing/SlimCheck/Testable.lean b/Mathlib/Testing/SlimCheck/Testable.lean index 2b5c1340f68ea..805db281cdfa2 100644 --- a/Mathlib/Testing/SlimCheck/Testable.lean +++ b/Mathlib/Testing/SlimCheck/Testable.lean @@ -510,7 +510,7 @@ quantifiers and add `NamedBinder` annotations next to them. -/ partial def addDecorations (e : Expr) : MetaM Expr := Meta.transform e fun expr => do if not (← Meta.inferType expr).isProp then - return .continue + return .done expr else if let Expr.forallE name type body data := expr then let newType ← addDecorations type let newBody ← Meta.withLocalDecl name data type fun fvar => do