From e12b129014f0416d7781e92b2d3eeae5481b70d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 Nov 2019 09:46:53 -0800
Subject: [PATCH] chore: add `usingDefault`

---
 library/Init/Lean/Meta/Basic.lean     | 3 +++
 library/Init/Lean/Meta/FunInfo.lean   | 2 +-
 library/Init/Lean/Meta/InferType.lean | 4 ++--
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/library/Init/Lean/Meta/Basic.lean b/library/Init/Lean/Meta/Basic.lean
index b3ca7e7ded..b33547a8d9 100644
--- a/library/Init/Lean/Meta/Basic.lean
+++ b/library/Init/Lean/Meta/Basic.lean
@@ -497,5 +497,8 @@ do mvarId ← mkFreshId;
    modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s };
    pure mvarId
 
+@[inline] def usingDefault (whnf : Expr → MetaM Expr) : Expr → MetaM Expr :=
+fun e => usingTransparency TransparencyMode.default $ whnf e
+
 end Meta
 end Lean
diff --git a/library/Init/Lean/Meta/FunInfo.lean b/library/Init/Lean/Meta/FunInfo.lean
index 7c9123e4f8..941da3fa65 100644
--- a/library/Init/Lean/Meta/FunInfo.lean
+++ b/library/Init/Lean/Meta/FunInfo.lean
@@ -58,7 +58,7 @@ else
     (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
 checkFunInfoCache fn maxArgs? $ do
   fnType ← inferTypeAux whnf fn;
-  forallBoundedTelescope (fun e => usingTransparency TransparencyMode.all $ whnf e) fnType maxArgs? $ fun fvars type => do
+  forallBoundedTelescope (usingDefault whnf) fnType maxArgs? $ fun fvars type => do
     pinfo ← fvars.size.foldM
       (fun (i : Nat) (pinfo : Array ParamInfo) => do
         let fvar := fvars.get! i;
diff --git a/library/Init/Lean/Meta/InferType.lean b/library/Init/Lean/Meta/InferType.lean
index e55373ebf0..7cec6a6313 100644
--- a/library/Init/Lean/Meta/InferType.lean
+++ b/library/Init/Lean/Meta/InferType.lean
@@ -165,7 +165,7 @@ do s ← get;
 @[inline] def inferTypeAux
     (whnf : Expr → MetaM Expr)
     (e : Expr) : MetaM Expr :=
-inferTypeAuxAux (fun e => usingTransparency TransparencyMode.all $ whnf e) e
+inferTypeAuxAux (usingDefault whnf) e
 
 /--
   Return `LBool.true` if given level is always equivalent to universe level zero.
@@ -235,7 +235,7 @@ do r ← isPropQuick e;
    | LBool.undef => do
      -- dbgTrace ("PropQuick failed " ++ toString e);
      type ← inferTypeAux whnf e;
-     type ← (fun e => usingTransparency TransparencyMode.all $ whnf e) type;
+     type ← usingDefault whnf type;
      match type with
      | Expr.sort u => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u
      | _           => pure false