refactor: more idiomatic syntax for if h:

src/Init/Data/ByteArray/Basic.lean

@@ -245,7 +245,7 @@ On an invalid position, returns `(default : UInt8)`. -/
 @[inline]
 def curr : Iterator → UInt8
   | ⟨arr, i⟩ =>
-    if h:i < arr.size then
+    if h : i < arr.size then
       arr[i]'h
     else
       default

src/Lean/Compiler/IR/SimpCase.lean

@@ -20,15 +20,15 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
   let aBody := (alts.get! i).body
   let mut n := 1
-  for h: j in [i+1:alts.size] do
+  for h : j in [i+1:alts.size] do
     if alts[j].body == aBody then
       n := n+1
   return n
 
 private def maxOccs (alts : Array Alt) : Alt × Nat := Id.run do
   let mut maxAlt := alts[0]!
   let mut max    := getOccsOf alts 0
-  for h: i in [1:alts.size] do
+  for h : i in [1:alts.size] do
     let curr := getOccsOf alts i
     if curr > max then
        maxAlt := alts[i]

src/Lean/Compiler/LCNF/Check.lean

@@ -110,7 +110,7 @@ def isCtorParam (f : Expr) (i : Nat) : CoreM Bool := do
 def checkAppArgs (f : Expr) (args : Array Arg) : CheckM Unit := do
   let mut fType ← inferType f
   let mut j := 0
-  for h: i in [:args.size] do
+  for h : i in [:args.size] do
     let arg := args[i]
     if fType.isErased then
       return ()

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -505,7 +505,7 @@ ones. Return whether any `Value` got updated in the process.
 -/
 def inferStep : InterpM Bool := do
   let ctx ← read
-  for h: idx in [0:ctx.decls.size] do
+  for h : idx in [0:ctx.decls.size] do
     let decl := ctx.decls[idx]
     if !decl.safe then
       continue

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -48,7 +48,7 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
   let [ctorName] := info.ctors | return none
   let mask ← getRelevantCtorFields ctorName
   let mut result := none
-  for h: i in [:mask.size] do
+  for h : i in [:mask.size] do
     if mask[i] then
       if result.isSome then return none
       result := some { ctorName, fieldIdx := i, numParams := info.numParams }

src/Lean/Compiler/LCNF/PullFunDecls.lean

@@ -96,7 +96,7 @@ where
     unless (← visited i) do
       modify fun (k, visited) => (k, visited.set! i true)
       let pi := ps[i]!
-      for h: j in [:ps.size] do
+      for h : j in [:ps.size] do
         unless (← visited j) do
           let pj := ps[j]
           if pj.used.contains pi.decl.fvarId then

src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean

@@ -18,7 +18,7 @@ or not.
 private def getMaxOccs (alts : Array Alt) : Alt × Nat := Id.run do
   let mut maxAlt := alts[0]!
   let mut max    := getNumOccsOf alts 0
-  for h: i in [1:alts.size] do
+  for h : i in [1:alts.size] do
     let curr := getNumOccsOf alts i
     if curr > max then
        maxAlt := alts[i]
@@ -34,7 +34,7 @@ where
   getNumOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
     let code := alts[i]!.getCode
     let mut n := 1
-    for h: j in [i+1:alts.size] do
+    for h : j in [i+1:alts.size] do
       if Code.alphaEqv alts[j].getCode code then
         n := n+1
     return n

src/Lean/Compiler/LCNF/Simp/JpCases.lean

@@ -121,7 +121,7 @@ where
     let mut paramsNew := #[]
     let singleton : FVarIdSet := ({} : FVarIdSet).insert params[targetParamIdx]!.fvarId
     let dependsOnDiscr := k.dependsOn singleton || decls.any (·.dependsOn singleton)
-    for h: i in [:params.size] do
+    for h : i in [:params.size] do
       let param := params[i]
       if targetParamIdx == i then
         if dependsOnDiscr then

src/Lean/Compiler/LCNF/SpecInfo.lean

@@ -129,7 +129,7 @@ See comment at `.fixedNeutral`.
 -/
 private def hasFwdDeps (decl : Decl) (paramsInfo : Array SpecParamInfo) (j : Nat) : Bool := Id.run do
   let param := decl.params[j]!
-  for h: k in [j+1 : decl.params.size] do
+  for h : k in [j+1 : decl.params.size] do
     if paramsInfo[k]! matches .user | .fixedHO | .fixedInst then
       let param' := decl.params[k]
       if param'.type.containsFVar param.fvarId then

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -50,7 +50,7 @@ partial def inlineMatchers (e : Expr) : CoreM Expr :=
       let numAlts := info.numAlts
       let altNumParams := info.altNumParams
       let rec inlineMatcher (i : Nat) (args : Array Expr) (letFVars : Array Expr) : MetaM Expr := do
-        if h: i < numAlts then
+        if h : i < numAlts then
           let altIdx := i + info.getFirstAltPos
           let numParams := altNumParams[i]
           let alt ← normalizeAlt args[altIdx]! numParams

src/Lean/Elab/App.lean

@@ -421,7 +421,7 @@ private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do
   else
     forallTelescopeReducing s.fType fun xs _ => do
       let curr := xs[0]!
-      for h: i in [1:xs.size] do
+      for h : i in [1:xs.size] do
         let xDecl ← xs[i].fvarId!.getDecl
         if let some arg := s.namedArgs.find? fun arg => arg.name == xDecl.userName then
           /- Remark: a default value at `optParam` does not count as a dependency -/
@@ -800,7 +800,7 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
         return s
     /- Collect the major parameter positions -/
     let mut majorsPos := #[]
-    for h: i in [:xs.size] do
+    for h : i in [:xs.size] do
       let x := xs[i]
       unless motivePos == i do
         let xType ← x.fvarId!.getType
@@ -1301,7 +1301,7 @@ private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Ar
   forallTelescopeReducing fType fun xs _ => do
     let mut argIdx := 0 -- position of the next explicit argument
     let mut remainingNamedArgs := namedArgs
-    for h: i in [:xs.size] do
+    for h : i in [:xs.size] do
       let x := xs[i]
       let xDecl ← x.fvarId!.getDecl
       /- If there is named argument with name `xDecl.userName`, then we skip it. -/

src/Lean/Elab/BuiltinNotation.lean

@@ -55,7 +55,7 @@ open Meta
             let cinfo ← getConstInfoCtor ctor
             let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do
               let mut n := 0
-              for h: i in [cinfo.numParams:xs.size] do
+              for h : i in [cinfo.numParams:xs.size] do
                 if (← getFVarLocalDecl xs[i]).binderInfo.isExplicit then
                   n := n + 1
               return n

src/Lean/Elab/DeclNameGen.lean

@@ -64,7 +64,7 @@ private partial def winnowExpr (e : Expr) : MetaM Expr := do
         let mut fty ← inferType f
         let mut j := 0
         let mut e' ← visit f
-        for h: i in [0:args.size] do
+        for h : i in [0:args.size] do
           unless fty.isForall do
             fty ← withTransparency .all <| whnf <| fty.instantiateRevRange j i args
             j := i

src/Lean/Elab/Deriving/Inhabited.lean

@@ -86,7 +86,7 @@ where
       addLocalInstancesForParams xs[:ctorVal.numParams] fun localInst2Index => do
         let mut usedInstIdxs := {}
         let mut ok := true
-        for h: i in [ctorVal.numParams:xs.size] do
+        for h : i in [ctorVal.numParams:xs.size] do
           let x := xs[i]
           let instType ← mkAppM `Inhabited #[(← inferType x)]
           trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'"

src/Lean/Elab/Deriving/Repr.lean

@@ -29,7 +29,7 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
     let mut fields ← `(Format.nil)
     if xs.size != numParams + fieldNames.size then
       throwError "'deriving Repr' failed, unexpected number of fields in structure"
-    for h: i in [:fieldNames.size] do
+    for h : i in [:fieldNames.size] do
       let fieldName := fieldNames[i]
       let fieldNameLit := Syntax.mkStrLit (toString fieldName)
       let x := xs[numParams + i]!
@@ -59,7 +59,7 @@ where
         let mut ctorArgs := #[]
         let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name)
         rhs ← `(Format.text $rhs)
-        for h: i in [:xs.size] do
+        for h : i in [:xs.size] do
           -- Note: some inductive parameters are explicit if they were promoted from indices,
           -- so we process all constructor arguments in the same loop.
           let x := xs[i]

src/Lean/Elab/Do.lean

@@ -513,7 +513,7 @@ partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code :=
     | .ite ref none o c t e => return .ite ref none o c (← update t) (← update e)
     | .ite ref (some h) o cond t e =>
       if ws.contains h.getId then
-        -- if the `h` at `if h:c then t else e` shadows a variable in `ws`, we `pullExitPoints`
+        -- if the `h` at `if h : c then t else e` shadows a variable in `ws`, we `pullExitPoints`
         pullExitPoints c
       else
         return Code.ite ref (some h) o cond (← update t) (← update e)

src/Lean/Elab/Inductive.lean

@@ -168,7 +168,7 @@ private def checkHeader (r : ElabHeaderResult) (numParams : Nat) (firstType? : O
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 private partial def checkHeaders (rs : Array ElabHeaderResult) (numParams : Nat) (i : Nat) (firstType? : Option Expr) : TermElabM Unit := do
-  if h: i < rs.size then
+  if h : i < rs.size then
     let type ← checkHeader rs[i] numParams firstType?
     checkHeaders rs numParams (i+1) type
 
@@ -222,7 +222,7 @@ private def replaceArrowBinderNames (type : Expr) (newNames : Array Name) : Expr
   go type 0
 where
   go (type : Expr) (i : Nat) : Expr :=
-    if h: i < newNames.size then
+    if h : i < newNames.size then
       match type with
       | .forallE n d b bi =>
         if n.hasMacroScopes then

src/Lean/Elab/Match.lean

@@ -330,7 +330,7 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
   withReader (fun ctx => { ctx with implicitLambda := false }) do
     let mut patterns  := #[]
     let mut matchType := matchType
-    for h: idx in [:patternStxs.size] do
+    for h : idx in [:patternStxs.size] do
       let patternStx := patternStxs[idx]
       matchType ← whnf matchType
       match matchType with

src/Lean/Elab/MutualDef.lean

@@ -406,7 +406,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
       (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do
       forallBoundedTelescope header.type header.numParams fun xs type => do
         -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
-        for h: i in [0:header.binderIds.size] do
+        for h : i in [0:header.binderIds.size] do
           -- skip auto-bound prefix in `xs`
           addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
         let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -77,7 +77,7 @@ def mkEqns (declName : Name) (info : DefinitionVal) : MetaM (Array Name) :=
     withReducible do
       mkEqnTypes #[] goal.mvarId!
   let mut thmNames := #[]
-  for h: i in [: eqnTypes.size] do
+  for h : i in [: eqnTypes.size] do
     let type := eqnTypes[i]
     trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -67,7 +67,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     mkEqnTypes info.declNames goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
-  for h: i in [: eqnTypes.size] do
+  for h : i in [: eqnTypes.size] do
     let type := eqnTypes[i]
     trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -83,7 +83,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     withReducible do
       mkEqnTypes info.declNames goal.mvarId!
   let mut thmNames := #[]
-  for h: i in [: eqnTypes.size] do
+  for h : i in [: eqnTypes.size] do
     let type := eqnTypes[i]
     trace[Elab.definition.wf.eqns] "{eqnTypes[i]}"
     let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)

src/Lean/Elab/Quotation.lean

@@ -655,7 +655,7 @@ The parameter `alts` provides position information for alternatives.
 -/
 private def checkUnusedAlts (stx : Syntax) (alts : Array Syntax) (altIdxMap : NameMap Nat) (ignoreIfUnused : IdxSet) : TermElabM Syntax := do
   let (stx, used) ← findUsedAlts stx altIdxMap
-  for h: i in [:alts.size] do
+  for h : i in [:alts.size] do
     unless used.contains i || ignoreIfUnused.contains i do
       logErrorAt alts[i] s!"redundant alternative #{i+1}"
   return stx

src/Lean/Elab/SyntheticMVars.lean

@@ -257,7 +257,7 @@ private def throwStuckAtUniverseCnstr : TermElabM Unit := do
     unless found.contains (lhs, rhs) do
       found := found.insert (lhs, rhs)
       uniqueEntries := uniqueEntries.push entry
-  for h: i in [1:uniqueEntries.size] do
+  for h : i in [1:uniqueEntries.size] do
     logErrorAt uniqueEntries[i].ref (← mkLevelStuckErrorMessage uniqueEntries[i]!)
   throwErrorAt uniqueEntries[0]!.ref (← mkLevelStuckErrorMessage uniqueEntries[0]!)
 

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean

@@ -89,7 +89,7 @@ where
       M (Option ReifiedBVPred) := do
     let some lhs ← ReifiedBVExpr.of lhsExpr | return none
     let some rhs ← ReifiedBVExpr.of rhsExpr | return none
-    if h:lhs.width = rhs.width then
+    if h : lhs.width = rhs.width then
       let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr)
       let expr :=
         mkApp4

src/Lean/Elab/Tactic/Induction.lean

@@ -205,7 +205,7 @@ private def isWildcard (altStx : Syntax) : Bool :=
   getAltName altStx == `_
 
 private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
-  for h: i in [:altsSyntax.size] do
+  for h : i in [:altsSyntax.size] do
     let altStx := altsSyntax[i]
     if getAltName altStx == `_ && i != altsSyntax.size - 1 then
       withRef altStx <| throwError "invalid occurrence of wildcard alternative, it must be the last alternative"
@@ -236,7 +236,7 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
     let altVars := getAltVars altStx
     for fvarId in fvarIds do
       if !useNamesForExplicitOnly || (← fvarId.getDecl).binderInfo.isExplicit then
-        if h: i < altVars.size then
+        if h : i < altVars.size then
           Term.addLocalVarInfo altVars[i] (mkFVar fvarId)
           i := i + 1
 
@@ -320,7 +320,7 @@ where
     2- The errors are produced in the same order the appear in the code above. This is not super
     important when using IDEs.
     -/
-    for h: altStxIdx in [0:altStxs.size] do
+    for h : altStxIdx in [0:altStxs.size] do
       let altStx := altStxs[altStxIdx]
       let altName := getAltName altStx
       if let some i := alts.findIdx? (·.1 == altName) then

src/Lean/Elab/Tactic/Omega/Core.lean

@@ -513,7 +513,7 @@ def fourierMotzkinSelect (data : Array FourierMotzkinData) : MetaM FourierMotzki
   if bestSize = 0 then
     trace[omega] "Selected variable {data[0]!.var}."
     return data[0]!
-  for h: i in [1:data.size] do
+  for h : i in [1:data.size] do
     let exact := data[i].exact
     let size := data[i].size
     if size = 0 || !bestExact && exact || (bestExact == exact) && size < bestSize then

src/Lean/Environment.lean

@@ -765,7 +765,7 @@ where
   loop (i : Nat) (env : Environment) : IO Environment := do
     -- Recall that the size of the array stored `persistentEnvExtensionRef` may increase when we import user-defined environment extensions.
     let pExtDescrs ← persistentEnvExtensionsRef.get
-    if h: i < pExtDescrs.size then
+    if h : i < pExtDescrs.size then
       let extDescr := pExtDescrs[i]
       let s := extDescr.toEnvExtension.getState env
       let prevSize := (← persistentEnvExtensionsRef.get).size
@@ -858,7 +858,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
     numConsts + mod.constants.size + mod.extraConstNames.size
   let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.empty (capacity := numConsts)
   let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.empty (capacity := numConsts)
-  for h:modIdx in [0:s.moduleData.size] do
+  for h : modIdx in [0:s.moduleData.size] do
     let mod := s.moduleData[modIdx]'h.upper
     for cname in mod.constNames, cinfo in mod.constants do
       match constantMap.getThenInsertIfNew? cname cinfo with

src/Lean/LocalContext.lean

@@ -385,13 +385,13 @@ def size (lctx : LocalContext) : Nat :=
   Id.run <| lctx.findDeclRevM? f
 
 partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) : Bool :=
-  if h: i < a₁.size then
+  if h : i < a₁.size then
     match a₁[i] with
     | none       => isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) j
     | some decl₁ =>
       if exceptFVars.any fun fvar => fvar.fvarId! == decl₁.fvarId then
         isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) j
-      else if h2: j < a₂.size then
+      else if h2 : j < a₂.size then
         match a₂[j] with
         | none       => isSubPrefixOfAux a₁ a₂ exceptFVars i (j+1)
         | some decl₂ => if decl₁.fvarId == decl₂.fvarId then isSubPrefixOfAux a₁ a₂ exceptFVars (i+1) (j+1) else isSubPrefixOfAux a₁ a₂ exceptFVars i (j+1)

src/Lean/Meta/ACLt.lean

@@ -155,7 +155,7 @@ where
           if !infos[i]!.isInstImplicit then
             if !(← lt args[i]! b) then
               return false
-        for h: i in [infos.size:args.size] do
+        for h : i in [infos.size:args.size] do
           if !(← lt args[i] b) then
             return false
         return true

src/Lean/Meta/AppBuilder.lean

@@ -277,7 +277,7 @@ private def mkAppMFinal (methodName : Name) (f : Expr) (args : Array Expr) (inst
 
 private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : MetaM Expr :=
   let rec loop (type : Expr) (i : Nat) (j : Nat) (args : Array Expr) (instMVars : Array MVarId) : MetaM Expr := do
-    if h: i >= xs.size then
+    if h : i >= xs.size then
       mkAppMFinal `mkAppM f args instMVars
     else match type with
       | Expr.forallE n d b bi =>

src/Lean/Meta/ArgsPacker.lean

@@ -69,7 +69,7 @@ The `type` should be the expected type of the packed argument, as created with `
 partial def pack (type : Expr) (args : Array Expr) : Expr := go 0 type
 where
   go (i : Nat) (type : Expr) : Expr :=
-    if h: i < args.size - 1 then
+    if h : i < args.size - 1 then
       let arg := args[i]
       assert! type.isAppOfArity ``PSigma 2
       let us := type.getAppFn.constLevels!

src/Lean/Meta/CongrTheorems.lean

@@ -185,7 +185,7 @@ private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := d
   forallTelescopeReducing val.type (cleanupAnnotations := true) fun xs _ => do
     let env ← getEnv
     let mut mask := #[]
-    for h: i in [:xs.size] do
+    for h : i in [:xs.size] do
       if i < val.numParams then
         mask := mask.push false
       else
@@ -211,7 +211,7 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) :
   -/
   let mut result := #[]
   let mask? ← getClassSubobjectMask? f
-  for h: i in [:info.paramInfo.size] do
+  for h : i in [:info.paramInfo.size] do
     if info.resultDeps.contains i then
       result := result.push .fixed
     else if info.paramInfo[i].isProp then