chore: add usingDefault

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

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;

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