From b4df4f025690e0e8b858f9acf6e88d2446eba8bc Mon Sep 17 00:00:00 2001 From: Abdalrhman M Mohamed Date: Thu, 9 Jan 2025 21:07:28 -0800 Subject: [PATCH] Auto changes. --- Test/Auto.expected | 4 ---- Test/Auto.lean | 2 ++ 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/Test/Auto.expected b/Test/Auto.expected index fdf406b4..e69de29b 100644 --- a/Test/Auto.expected +++ b/Test/Auto.expected @@ -1,4 +0,0 @@ -Test/Auto.lean:38:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!9 (!13 (!1 !2)) !3) = (!0 (!1 !2) !3)) is not type correct -Test/Auto.lean:41:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!11 (!1 (!2 !3))) !3) = (!0 (!1 (!2 !3)) !3)) is not type correct -Test/Auto.lean:44:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!10 (!1 (!2 !3))) !3) = (!0 (!1 (!2 !3)) !3)) is not type correct -Test/Auto.lean:48:2: error: Auto.LamReif.reifTermCheckType :: LamTerm ((!6 (!10 !1) (!2 (!3 !1))) = (!0 !1 (!2 (!3 !1)))) is not type correct diff --git a/Test/Auto.lean b/Test/Auto.lean index 0bca5826..c1d74583 100644 --- a/Test/Auto.lean +++ b/Test/Auto.lean @@ -31,6 +31,8 @@ theorem unique_identity (e : G) : (∀ z, e * z = z) → e = 1 := by -- auto d[List.get?] set_option auto.mono.mode "fol" +set_option auto.mono.ciInstDefEq.mode "reducible" +set_option auto.mono.termLikeDefEq.mode "reducible" variable [Nonempty α] [Nonempty β] {f : α → β} {s : Set α} {v u : Set β}