From ea2d971bd3299b55fc07e16c0ca061fd49920590 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 Nov 2019 11:54:06 -0800
Subject: [PATCH] chore: add `isDefEq` abbreviation for `isExprDefEq`

Most tactic users will never use `isLevelDefEq`.
---
 src/Init/Lean/Meta/ExprDefEq.lean | 2 ++
 tests/lean/run/meta2.lean         | 4 ++--
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index 4e3d2d01c0..3b61289b90 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -999,5 +999,7 @@ partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
 @[init] def setIsExprDefEqAuxRef : IO Unit :=
 isExprDefEqAuxRef.set isExprDefEqAuxImpl
 
+abbrev isDefEq := @isExprDefEq
+
 end Meta
 end Lean
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 3641be1c20..fd31eef6c0 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -177,8 +177,8 @@ do print "----- tst6 -----";
      m2 ← mkFreshExprMVar type;
      let t := mkApp io x;
      -- we need to use foApprox to solve `?m1 ?m2 =?= IO x`
-     check $ not <$> isExprDefEq (mkApp m1 m2) t;
-     check $ approxDefEq $ isExprDefEq (mkApp m1 m2) t;
+     check $ not <$> isDefEq (mkApp m1 m2) t;
+     check $ approxDefEq $ isDefEq (mkApp m1 m2) t;
      v ← getAssignment m1;
      check $ pure $ v == io;
      v ← getAssignment m2;