minor update

leanprover-community · Dec 27, 2024 · d428dfa · d428dfa
1 parent ed277c2
commit d428dfa
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 2 deletions.
diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
@@ -41,7 +41,7 @@ register_option auto.mono.ciInstDefEq.mode : Meta.TransparencyMode := {
 }
 
 register_option auto.mono.ciInstDefEq.maxHeartbeats : Nat := {
-  defValue := 1024
+  defValue := 2048
   descr := "Heartbeats allocated to each unification of constant instance"
 }
 
@@ -52,7 +52,7 @@ register_option auto.mono.termLikeDefEq.mode : Meta.TransparencyMode := {
 }
 
 register_option auto.mono.termLikeDefEq.maxHeartbeats : Nat := {
-  defValue := 1024
+  defValue := 2048
   descr := "Heartbeats allocated to each unification of term-like expression"
 }
 

diff --git a/Test/Test_Regression.lean b/Test/Test_Regression.lean
@@ -277,6 +277,9 @@ end UnfoldConst
 
 section ConstInstDefEq
 
+  -- Effectively disable `termLikeDefEq`
+  set_option auto.mono.termLikeDefEq.mode "reducible"
+
   def Nat.add₁ := Nat.add
 
   example : Nat.add₁ = Nat.add := by
@@ -312,6 +315,16 @@ section ConstInstDefEq
 
 end ConstInstDefEq
 
+-- Definitional Equality from Term-like expressions
+
+section TermLikeDefEq
+
+  set_option auto.tptp false
+  example (h : List.append [1, 2] [3, 4] = [2, 3]) : [1, 2, 3, 4] = [2, 3] := by
+    auto
+
+end TermLikeDefEq
+
 -- First Order
 
 example : True := by