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

chore: improve compatibility of tests/list_simp with Mathlib (#4691)

Browse source 
I'd like to be able to automatically re-test simp normal forms
post-Mathlib. This makes the file compatible with Mathlib.
This commit is contained in:
Kim Morrison 2024-07-09 03:17:28 +10:00 • committed by GitHub
parent aecebaab74
commit 84c40d9999
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/list_simp.lean
View file

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