From a1f0e7d8e6cef2f36681abf2e96f6ea6a0a4478e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Nov 2019 10:41:53 -0800
Subject: [PATCH] chore: add `approxDefEq` and more tracing

---
 library/Init/Lean/Meta/Basic.lean     | 6 ++++++
 library/Init/Lean/Meta/ExprDefEq.lean | 3 ++-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/library/Init/Lean/Meta/Basic.lean b/library/Init/Lean/Meta/Basic.lean
index 91189c51ce..280ce0060f 100644
--- a/library/Init/Lean/Meta/Basic.lean
+++ b/library/Init/Lean/Meta/Basic.lean
@@ -63,6 +63,7 @@ abbrev LocalInstances := Array LocalInstance
 
 structure Config :=
 (opts               : Options := {})
+-- TODO: merge all *Approx flags.
 (foApprox           : Bool    := false)
 (ctxApprox          : Bool    := false)
 (quasiPatternApprox : Bool    := false)
@@ -603,5 +604,10 @@ do mvarId ← mkFreshId;
 def whnfUsingDefault : Expr → MetaM Expr :=
 fun e => usingTransparency TransparencyMode.default $ whnf e
 
+/-- Execute `x` using approximate unification. -/
+@[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
+adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true, .. ctx.config }, .. ctx })
+  x
+
 end Meta
 end Lean
diff --git a/library/Init/Lean/Meta/ExprDefEq.lean b/library/Init/Lean/Meta/ExprDefEq.lean
index 9575077a0e..7f7a0b0181 100644
--- a/library/Init/Lean/Meta/ExprDefEq.lean
+++ b/library/Init/Lean/Meta/ExprDefEq.lean
@@ -605,7 +605,8 @@ else
    def ITactic := Tactic Unit
 -/
 private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr) : Expr → MetaM Bool
-| v =>
+| v => do
+  trace! `Meta.isDefEq.foApprox (mvar ++ " " ++ args ++ " := " ++ v);
   condM (try $ processAssignmentFOApproxAux mvar args v)
     (pure true)
     (unfoldDefinitionAux v (pure false) processAssignmentFOApprox)