From 84c40d9999b15be950c8f94358ff72ede82cfebb Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 9 Jul 2024 03:17:28 +1000 Subject: [PATCH] chore: improve compatibility of tests/list_simp with Mathlib (#4691) I'd like to be able to automatically re-test simp normal forms post-Mathlib. This makes the file compatible with Mathlib. --- tests/lean/run/list_simp.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/lean/run/list_simp.lean b/tests/lean/run/list_simp.lean index 74fc3fa747..c087bcd168 100644 --- a/tests/lean/run/list_simp.lean +++ b/tests/lean/run/list_simp.lean @@ -1,4 +1,5 @@ -import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List +set_option autoImplicit false -- For compatibility with downstream projects, so we can retest after Mathlib. +set_option relaxedAutoImplicit false open List @@ -271,7 +272,7 @@ variable {p : α → Bool} (w : ¬ p x) (h : 0 < n) in -- findSome? #check_simp (replicate (n+1) x).findSome? (fun x => some x) ~> some x -#check_simp (replicate (n+1) x).findSome? (fun _ => none) ~> none +#check_simp (replicate (n+1) x).findSome? (fun _ => (none : Option β)) ~> none variable {f : α → Option β} (w : (f x).isSome) in #check_tactic (replicate (n+1) x).findSome? f ~> f x by simp [w] @@ -281,7 +282,7 @@ variable {f : α → Option β} (w : (f x).isNone) in variable (h : 0 < n) in #check_tactic (replicate n x).findSome? (fun x => some x) ~> some x by simp [h] variable (h : 0 < n) in -#check_tactic (replicate n x).findSome? (fun _ => none) ~> none by simp [h] +#check_tactic (replicate n x).findSome? (fun _ => (none : Option β)) ~> none by simp [h] variable {f : α → Option β} (w : (f x).isSome) (h : 0 < n) in #check_tactic (replicate n x).findSome? f ~> f x by simp [w, h]