chore: naming convention

src/Init/Lean/Meta/Basic.lean

@@ -260,12 +260,12 @@ ctx ← read; pure ctx.config.opts
 env ← getEnv; pure $ isReducible env constName
 
 /-- While executing `x`, ensure the given transparency mode is used. -/
-@[inline] def usingTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
+@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
 adaptReader
   (fun (ctx : Context) => { config := { transparency := mode, .. ctx.config }, .. ctx })
   x
 
-@[inline] def usingAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
+@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
 adaptReader
   (fun (ctx : Context) =>
     let oldMode := ctx.config.transparency;
@@ -557,7 +557,7 @@ else
   k #[] type
 
 partial def isClassExpensive : Expr → MetaM (Option Name)
-| type => usingTransparency TransparencyMode.reducible $ -- when testing whether a type is a type class, we only unfold reducible constants.
+| type => withTransparency TransparencyMode.reducible $ -- when testing whether a type is a type class, we only unfold reducible constants.
   forallTelescopeReducingAux isClassExpensive type none $ fun xs type => do
     match type.getAppFn with
     | Expr.const c _ _ => do
@@ -704,10 +704,8 @@ mvarId ← mkFreshId;
 modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s };
 pure mvarId
 
-def whnfUsingDefault : Expr → MetaM Expr :=
-fun e => usingTransparency TransparencyMode.default $ whnf e
-
-abbrev whnfD := whnfUsingDefault
+def whnfD : Expr → MetaM Expr :=
+fun e => withTransparency TransparencyMode.default $ whnf e
 
 /-- Execute `x` using approximate unification. -/
 @[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=

src/Init/Lean/Meta/Check.lean

@@ -79,7 +79,7 @@ private partial def checkAux : Expr → MetaM Unit
 
 def check (e : Expr) : MetaM Unit :=
 traceCtx `Meta.check $
-  usingTransparency TransparencyMode.all $ checkAux e
+  withTransparency TransparencyMode.all $ checkAux e
 
 def isTypeCorrect (e : Expr) : MetaM Bool :=
 catch

src/Init/Lean/Meta/DiscrTree.lean

@@ -182,7 +182,7 @@ partial def mkPathAux : Array Expr → Array Key → MetaM (Array Key)
 private def initCapacity := 8
 
 def mkPath (e : Expr) : MetaM (Array Key) :=
-usingTransparency TransparencyMode.reducible $ do
+withTransparency TransparencyMode.reducible $ do
   let todo : Array Expr := Array.mkEmpty initCapacity;
   let keys : Array Key  := Array.mkEmpty initCapacity;
   mkPathAux (todo.push e) keys
@@ -309,7 +309,7 @@ match d.root.find Key.star with
 | some (Trie.node vs _) => result ++ vs
 
 def getMatch {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
-usingTransparency TransparencyMode.reducible $ do
+withTransparency TransparencyMode.reducible $ do
   let result := getStarResult d;
   (k, args) ← getMatchKeyArgs e;
   match k with
@@ -341,7 +341,7 @@ private partial def getUnifyAux {α} : Nat → Array Expr → Trie α → (Array
       | some c => do result ← visitStarChild result; getUnifyAux 0 (todo ++ args) c.2 result
 
 def getUnify {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
-usingTransparency TransparencyMode.reducible $ do
+withTransparency TransparencyMode.reducible $ do
   (k, args) ← getUnifyKeyArgs e;
   match k with
   | Key.star => d.root.foldlM (fun result k c => getUnifyAux k.arity #[] c result) #[]

src/Init/Lean/Meta/ExprDefEq.lean

@@ -27,7 +27,7 @@ namespace Meta
 private def isDefEqEta (a b : Expr) : MetaM Bool :=
 if a.isLambda && !b.isLambda then do
   bType ← inferType b;
-  bType ← whnfUsingDefault bType;
+  bType ← whnfD bType;
   match bType with
   | Expr.forallE n d _ c =>
     let b' := Lean.mkLambda n c.binderInfo d (mkApp b (mkBVar 0));
@@ -128,7 +128,7 @@ if h : args₁.size = args₂.size then do
       synthPending a₂;
       pure ()
     };
-    usingAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂)
+    withAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂)
 else
   pure false
 
@@ -633,7 +633,7 @@ traceCtx `Meta.isDefEq.assign.checkTypes $ do
   -- must check whether types are definitionally equal or not, before assigning and returning true
   mvarType ← inferType mvar;
   vType    ← inferType v;
-  condM (usingTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
+  condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
     (do assignExprMVar mvar.mvarId! v; pure true)
     (do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
         pure false)
@@ -695,7 +695,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
            -- must check whether types are definitionally equal or not, before assigning and returning true
            mvarType ← inferType mvar;
            vType    ← inferType v;
-           condM (usingTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
+           condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
              (do assignExprMVar mvarId v; pure true)
              (do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
                  pure false)

src/Init/Lean/Meta/FunInfo.lean

@@ -56,7 +56,7 @@ else
 private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
 checkFunInfoCache fn maxArgs? $ do
   fnType ← inferType fn;
-  usingTransparency TransparencyMode.default $
+  withTransparency TransparencyMode.default $
     forallBoundedTelescope fnType maxArgs? $ fun fvars type => do
       pinfo ← fvars.size.foldM
         (fun (i : Nat) (pinfo : Array ParamInfo) => do

src/Init/Lean/Meta/InferType.lean

@@ -69,7 +69,7 @@ matchConst env structType.getAppFn failed $ fun structInfo structLvls => do
 
 def getLevel (type : Expr) : MetaM Level := do
 typeType ← inferType type;
-typeType ← whnfUsingDefault typeType;
+typeType ← whnfD typeType;
 match typeType with
 | Expr.sort lvl _    => pure lvl
 | Expr.mvar mvarId _ =>
@@ -141,7 +141,7 @@ private partial def inferTypeAux : Expr → MetaM Expr
 | Expr.localE _ _ _ _      => unreachable!
 
 def inferTypeImpl (e : Expr) : MetaM Expr :=
-usingTransparency TransparencyMode.default (inferTypeAux e)
+withTransparency TransparencyMode.default (inferTypeAux e)
 
 @[init] def setInferTypeRef : IO Unit :=
 inferTypeRef.set inferTypeImpl
@@ -215,7 +215,7 @@ match r with
 | LBool.undef => do
   -- dbgTrace ("isPropQuick failed " ++ toString e);
   type ← inferType e;
-  type ← whnfUsingDefault type;
+  type ← whnfD type;
   match type with
   | Expr.sort u _ => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u
   | _             => pure false
@@ -323,7 +323,7 @@ match r with
 | LBool.false => pure false
 | LBool.undef => do
   type ← inferType e;
-  type ← whnfUsingDefault type;
+  type ← whnfD type;
   match type with
   | Expr.sort _ _ => pure true
   | _             => pure false

src/Init/Lean/Meta/SynthInstance.lean

@@ -511,7 +511,7 @@ try $
   r.exprReplacements.allM (fun ⟨e, e'⟩ => isExprDefEqAux e e')
 
 def synthInstance? (type : Expr) (fuel : Nat := 10000) : MetaM (Option Expr) :=
-usingTransparency TransparencyMode.reducible $ do
+withTransparency TransparencyMode.reducible $ do
   type ← instantiateMVars type;
   type ← preprocess type;
   s ← get;