Auto changes.

ufmg-smite · Jan 10, 2025 · b4df4f0 · b4df4f0
1 parent 9722cdf
commit b4df4f0
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git 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
@@ -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 β}