max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: switch obvious cases of array "bang"[]! indexing to rely on hypothesis (#5552)

Browse source 
Update certain uses of `arr[i]!` to use the "provably correct" version
`arr[i]`, in order to use "best practices".

Some motivation and discussion on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.20compiler.2Felaborator.20development.20question/near/472934715)
This commit is contained in:
TomasPuverle 2024-10-01 04:12:22 -07:00 • committed by GitHub
parent 37baa89d9b
commit ddec5336e5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
41 changed files with 129 additions and 131 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Compiler/IR/SimpCase.lean
View file

@ -20,18 +20,18 @@ 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 j in [i+1:alts.size] do
if alts[j]!.body == aBody then
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 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]!
maxAlt := alts[i]
max := curr
return (maxAlt, max)

4
src/Lean/Compiler/LCNF/Check.lean
View file

@ -110,8 +110,8 @@ 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 i in [:args.size] do
let arg := args[i]!
for h: i in [:args.size] do
let arg := args[i]
if fType.isErased then
return ()
fType := fType.headBeta

4
src/Lean/Compiler/LCNF/ElimDeadBranches.lean
View file

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

6
src/Lean/Compiler/LCNF/MonoTypes.lean
View file

@ -48,8 +48,8 @@ def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo)
let [ctorName] := info.ctors | return none
let mask ← getRelevantCtorFields ctorName
let mut result := none
for i in [:mask.size] do
if mask[i]! then
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 }
return result
@ -129,4 +129,4 @@ def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
modifyEnv fun env => monoTypeExt.modifyState env fun s => { s with mono := s.mono.insert declName type }
return type
end Lean.Compiler.LCNF
end Lean.Compiler.LCNF

4
src/Lean/Compiler/LCNF/PullFunDecls.lean
View file

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

8
src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean
View file

@ -18,10 +18,10 @@ 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 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]!
maxAlt := alts[i]
max := curr
return (maxAlt, max)
where
@ -34,8 +34,8 @@ where
getNumOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do
let code := alts[i]!.getCode
let mut n := 1
for j in [i+1:alts.size] do
if Code.alphaEqv alts[j]!.getCode code then
for h: j in [i+1:alts.size] do
if Code.alphaEqv alts[j].getCode code then
n := n+1
return n

5
src/Lean/Compiler/LCNF/Simp/JpCases.lean
View file

@ -121,8 +121,8 @@ where
let mut paramsNew := #[]
let singleton : FVarIdSet := ({} : FVarIdSet).insert params[targetParamIdx]!.fvarId
let dependsOnDiscr := k.dependsOn singleton || decls.any (·.dependsOn singleton)
for i in [:params.size] do
let param := params[i]!
for h: i in [:params.size] do
let param := params[i]
if targetParamIdx == i then
if dependsOnDiscr then
paramsNew := paramsNew.push (← internalizeParam param)
@ -300,4 +300,3 @@ builtin_initialize
registerTraceClass `Compiler.simp.jpCases
end Lean.Compiler.LCNF

5
src/Lean/Compiler/LCNF/SpecInfo.lean
View file

@ -129,9 +129,9 @@ See comment at `.fixedNeutral`.
-/
private def hasFwdDeps (decl : Decl) (paramsInfo : Array SpecParamInfo) (j : Nat) : Bool := Id.run do
let param := decl.params[j]!
for 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]!
let param' := decl.params[k]
if param'.type.containsFVar param.fvarId then
return true
return false
@ -214,4 +214,3 @@ builtin_initialize
registerTraceClass `Compiler.specialize.info
end Lean.Compiler.LCNF

4
src/Lean/Compiler/LCNF/ToDecl.lean
View file

@ -50,9 +50,9 @@ 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 i < numAlts then
if h: i < numAlts then
let altIdx := i + info.getFirstAltPos
let numParams := altNumParams[i]!
let numParams := altNumParams[i]
let alt ← normalizeAlt args[altIdx]! numParams
Meta.withLetDecl (← mkFreshUserName `_alt) (← Meta.inferType alt) alt fun altFVar =>
inlineMatcher (i+1) (args.set! altIdx altFVar) (letFVars.push altFVar)

12
src/Lean/Elab/App.lean
View file

@ -421,8 +421,8 @@ private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do
else
forallTelescopeReducing s.fType fun xs _ => do
let curr := xs[0]!
for i in [1:xs.size] do
let xDecl ← xs[i]!.fvarId!.getDecl
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 -/
if (← exprDependsOn xDecl.type.cleanupAnnotations curr.fvarId!) then
@ -800,8 +800,8 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
return s
/- Collect the major parameter positions -/
let mut majorsPos := #[]
for i in [:xs.size] do
let x := xs[i]!
for h: i in [:xs.size] do
let x := xs[i]
unless motivePos == i do
let xType ← x.fvarId!.getType
/-
@ -1301,8 +1301,8 @@ 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 i in [:xs.size] do
let x := xs[i]!
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. -/
match remainingNamedArgs.findIdx? (fun namedArg => namedArg.name == xDecl.userName) with

4
src/Lean/Elab/BuiltinNotation.lean
View file

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

4
src/Lean/Elab/DeclNameGen.lean
View file

@ -64,13 +64,13 @@ private partial def winnowExpr (e : Expr) : MetaM Expr := do
let mut fty ← inferType f
let mut j := 0
let mut e' ← visit f
for 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
let .forallE _ _ fty' bi := fty | failure
fty := fty'
let arg := args[i]!
let arg := args[i]
if ← pure bi.isExplicit <||> (pure !arg.isSort <&&> isTypeFormer arg) then
unless (← isProof arg) do
e' := .app e' (← visit arg)

4
src/Lean/Elab/Deriving/Inhabited.lean
View file

@ -86,8 +86,8 @@ where
addLocalInstancesForParams xs[:ctorVal.numParams] fun localInst2Index => do
let mut usedInstIdxs := {}
let mut ok := true
for i in [ctorVal.numParams:xs.size] do
let x := xs[i]!
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}'"
match (← trySynthInstance instType) with

8
src/Lean/Elab/Deriving/Repr.lean
View file

@ -29,8 +29,8 @@ 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 i in [:fieldNames.size] do
let fieldName := fieldNames[i]!
for h: i in [:fieldNames.size] do
let fieldName := fieldNames[i]
let fieldNameLit := Syntax.mkStrLit (toString fieldName)
let x := xs[numParams + i]!
if i != 0 then
@ -59,10 +59,10 @@ where
let mut ctorArgs := #[]
let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name)
rhs ← `(Format.text $rhs)
for 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]!
let x := xs[i]
let a ← mkIdent <$> if i < indVal.numParams then pure header.argNames[i]! else mkFreshUserName `a
if i < indVal.numParams then
-- add `_` for inductive parameters, they are inaccessible

8
src/Lean/Elab/Inductive.lean
View file

@ -168,8 +168,8 @@ 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 i < rs.size then
let type ← checkHeader rs[i]! numParams firstType?
if h: i < rs.size then
let type ← checkHeader rs[i] numParams firstType?
checkHeaders rs numParams (i+1) type
private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHeaderResult) := do
@ -222,11 +222,11 @@ private def replaceArrowBinderNames (type : Expr) (newNames : Array Name) : Expr
go type 0
where
go (type : Expr) (i : Nat) : Expr :=
if i < newNames.size then
if h: i < newNames.size then
match type with
| .forallE n d b bi =>
if n.hasMacroScopes then
mkForall newNames[i]! bi d (go b (i+1))
mkForall newNames[i] bi d (go b (i+1))
else
mkForall n bi d (go b (i+1))
| _ => type

4
src/Lean/Elab/Match.lean
View file

@ -330,8 +330,8 @@ 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 idx in [:patternStxs.size] do
let patternStx := patternStxs[idx]!
for h: idx in [:patternStxs.size] do
let patternStx := patternStxs[idx]
matchType ← whnf matchType
match matchType with
| Expr.forallE _ d b _ =>

4
src/Lean/Elab/MutualDef.lean
View file

@ -406,9 +406,9 @@ 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 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]!
addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]!
let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
-- synthesize mvars here to force the top-level tactic block (if any) to run
elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing

6
src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
View file

@ -77,9 +77,9 @@ def mkEqns (declName : Name) (info : DefinitionVal) : MetaM (Array Name) :=
withReducible do
mkEqnTypes #[] goal.mvarId!
let mut thmNames := #[]
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]!}"
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)
thmNames := thmNames.push name
let value ← mkProof declName type

4
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View file

@ -67,8 +67,8 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
mkEqnTypes info.declNames goal.mvarId!
let baseName := info.declName
let mut thmNames := #[]
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
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)
thmNames := thmNames.push name

6
src/Lean/Elab/PreDefinition/WF/Eqns.lean
View file

@ -83,9 +83,9 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
withReducible do
mkEqnTypes info.declNames goal.mvarId!
let mut thmNames := #[]
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
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)
thmNames := thmNames.push name
let value ← mkProof declName type

4
src/Lean/Elab/Quotation.lean
View file

@ -655,9 +655,9 @@ 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 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}"
logErrorAt alts[i] s!"redundant alternative #{i+1}"
return stx
def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do

4
src/Lean/Elab/SyntheticMVars.lean
View file

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

12
src/Lean/Elab/Tactic/Induction.lean
View file

@ -205,8 +205,8 @@ private def isWildcard (altStx : Syntax) : Bool :=
getAltName altStx == `_
private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
for i in [:altsSyntax.size] do
let altStx := altsSyntax[i]!
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"
let altName := getAltName altStx
@ -236,8 +236,8 @@ 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 i < altVars.size then
Term.addLocalVarInfo altVars[i]! (mkFVar fvarId)
if h: i < altVars.size then
Term.addLocalVarInfo altVars[i] (mkFVar fvarId)
i := i + 1
open Language in
@ -320,8 +320,8 @@ 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 altStxIdx in [0:altStxs.size] do
let altStx := altStxs[altStxIdx]!
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
-- cover named alternative

10
src/Lean/Elab/Tactic/Omega/Core.lean
View file

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

4
src/Lean/Environment.lean
View file

@ -765,8 +765,8 @@ 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 i < pExtDescrs.size then
let extDescr := pExtDescrs[i]!
if h: i < pExtDescrs.size then
let extDescr := pExtDescrs[i]
let s := extDescr.toEnvExtension.getState env
let prevSize := (← persistentEnvExtensionsRef.get).size
let prevAttrSize ← getNumBuiltinAttributes

8
src/Lean/LocalContext.lean
View file

@ -385,14 +385,14 @@ 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 i < a₁.size then
match a₁[i]! with
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 j < a₂.size then
match a₂[j]! with
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)
else false

4
src/Lean/Meta/ACLt.lean
View file

@ -155,8 +155,8 @@ where
if !infos[i]!.isInstImplicit then
if !(← lt args[i]! b) then
return false
for i in [infos.size:args.size] do
if !(← lt args[i]! b) then
for h: i in [infos.size:args.size] do
if !(← lt args[i] b) then
return false
return true
| .lam _ d e .. => lt d b <&&> lt e b

4
src/Lean/Meta/AppBuilder.lean
View file

@ -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 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 =>
@ -293,7 +293,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
let mvar ← mkFreshExprMVar d MetavarKind.synthetic n
loop b i j (args.push mvar) (instMVars.push mvar.mvarId!)
| _ =>
let x := xs[i]!
let x := xs[i]
let xType ← inferType x
if (← isDefEq d xType) then
loop b (i+1) j (args.push x) instMVars

4
src/Lean/Meta/ArgsPacker.lean
View file

@ -69,8 +69,8 @@ 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 i < args.size - 1 then
let arg := args[i]!
if h: i < args.size - 1 then
let arg := args[i]
assert! type.isAppOfArity ``PSigma 2
let us := type.getAppFn.constLevels!
let α := type.appFn!.appArg!

14
src/Lean/Meta/CongrTheorems.lean
View file

@ -77,7 +77,7 @@ partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem :=
where
withNewEqs {α} (xs ys : Array Expr) (k : Array Expr → Array CongrArgKind → MetaM α) : MetaM α :=
let rec loop (i : Nat) (eqs : Array Expr) (kinds : Array CongrArgKind) := do
if i < xs.size then
if i < xs.size then
let x := xs[i]!
let y := ys[i]!
let xType := (← inferType x).cleanupAnnotations
@ -185,11 +185,11 @@ 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 i in [:xs.size] do
for h: i in [:xs.size] do
if i < val.numParams then
mask := mask.push false
else
let localDecl ← xs[i]!.fvarId!.getDecl
let localDecl ← xs[i].fvarId!.getDecl
mask := mask.push (isSubobjectField? env val.induct localDecl.userName).isSome
return some mask
@ -211,14 +211,14 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) :
-/
let mut result := #[]
let mask? ← getClassSubobjectMask? f
for 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
else if info.paramInfo[i].isProp then
result := result.push .cast
else if info.paramInfo[i]!.isInstImplicit then
else if info.paramInfo[i].isInstImplicit then
if let some mask := mask? then
if h : i < mask.size then
if h2 : i < mask.size then
if mask[i] then
-- Parameter is a subobect field of a class constructor. See comment above.
result := result.push .eq

12
src/Lean/Meta/ExprDefEq.lean
View file

@ -80,19 +80,19 @@ where
checkpointDefEq do
let args := b.getAppArgs
let params := args[:ctorVal.numParams].toArray
for i in [ctorVal.numParams : args.size] do
for h: i in [ctorVal.numParams : args.size] do
let j := i - ctorVal.numParams
let proj ← mkProjFn ctorVal us params j a
if ← isProof proj then
unless ← isAbstractedUnassignedMVar args[i]! do
unless ← isAbstractedUnassignedMVar args[i] do
-- Skip expensive unification problem that is likely solved
-- using proof irrelevance. We already know that `proj` and
-- `args[i]!` have the same type, so they're defeq in any case.
-- `args[i]` have the same type, so they're defeq in any case.
-- See comment at `isAbstractedUnassignedMVar`.
continue
trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]!}"
unless (← isDefEq proj args[i]!) do
trace[Meta.isDefEq.eta.struct] "failed, unexpected arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]!}"
trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]}"
unless (← isDefEq proj args[i]) do
trace[Meta.isDefEq.eta.struct] "failed, unexpected arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]}"
return false
return true
else

8
src/Lean/Meta/FunInfo.lean
View file

@ -59,8 +59,8 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
forallBoundedTelescope fnType maxArgs? fun fvars type => do
let mut paramInfo := #[]
let mut higherOrderOutParams : FVarIdSet := {}
for i in [:fvars.size] do
let fvar := fvars[i]!
for h: i in [:fvars.size] do
let fvar := fvars[i]
let decl ← getFVarLocalDecl fvar
let backDeps := collectDeps fvars decl.type
let dependsOnHigherOrderOutParam :=
@ -79,9 +79,9 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
if let some outParamPositions := getOutParamPositions? (← getEnv) className then
unless outParamPositions.isEmpty do
let args := decl.type.getAppArgs
for i in [:args.size] do
for h2: i in [:args.size] do
if outParamPositions.contains i then
let arg := args[i]!
let arg := args[i]
if let some idx := fvars.indexOf? arg then
if (← whnf (← inferType arg)).isForall then
paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true }

8
src/Lean/Meta/IndPredBelow.lean
View file

@ -119,8 +119,8 @@ where
modifyBinders { vars with target := vars.target ++ xs, motives := xs } 0
modifyBinders (vars : Variables) (i : Nat) := do
if i < vars.args.size then
let binder := vars.args[i]!
if h: i < vars.args.size then
let binder := vars.args[i]
let binderType ← inferType binder
if (← checkCount binderType) then
mkBelowBinder vars binder binderType fun indValIdx x =>
@ -372,8 +372,8 @@ where
(rest : Expr)
(belowIndices : Array Nat)
(xIdx yIdx : Nat) : MetaM $ Array Nat := do
if xIdx ≥ xs.size then return belowIndices else
let x := xs[xIdx]!
if h: xIdx ≥ xs.size then return belowIndices else
let x := xs[xIdx]
let xTy ← inferType x
let yTy := rest.bindingDomain!
if (← isDefEq xTy yTy) then

8
src/Lean/Meta/PProdN.lean
View file

@ -115,8 +115,8 @@ It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no ex
-/
def packLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
if es.size = 1 then
return es[0]!
if h: es.size = 1 then
return es[0]
forallTelescope type fun xs sort => do
assert! sort.isSort
-- NB: Use beta, not instantiateLambda; when constructing the belowDict below
@ -131,8 +131,8 @@ The value analogue to `PProdN.packLambdas`.
It is the identity if `es.size = 1`.
-/
def mkLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
if es.size = 1 then
return es[0]!
if h: es.size = 1 then
return es[0]
forallTelescope type fun xs body => do
let lvl ← getLevel body
let es' := es.map (·.beta xs)

4
src/Lean/Meta/RecursorInfo.lean
View file

@ -182,13 +182,13 @@ private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl :
private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do
let mut produceMotive := #[]
let mut recursor := false
for i in [:xs.size] do
for h: i in [:xs.size] do
if i < numParams + 1 then
continue --skip parameters and motive
if majorPos - numIndices ≤ i && i ≤ majorPos then
continue -- skip indices and major premise
-- process minor premise
let x := xs[i]!
let x := xs[i]
let xType ← inferType x
(produceMotive, recursor) ← forallTelescopeReducing xType fun minorArgs minorResultType => minorResultType.withApp fun res _ => do
let produceMotive := produceMotive.push (res == motive)

4
src/Lean/Meta/Reduce.lean
View file

@ -26,8 +26,8 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
let finfo ← getFunInfoNArgs f nargs
let mut args := e.getAppArgs
for i in [:args.size] do
if i < finfo.paramInfo.size then
let info := finfo.paramInfo[i]!
if h: i < finfo.paramInfo.size then
let info := finfo.paramInfo[i]
if !explicitOnly || info.isExplicit then
args ← args.modifyM i visit
else

8
src/Lean/Meta/SizeOf.lean
View file

@ -16,8 +16,8 @@ private partial def mkLocalInstances (params : Array Expr) (k : Array Expr → M
loop 0 #[]
where
loop (i : Nat) (insts : Array Expr) : MetaM α := do
if i < params.size then
let param := params[i]!
if h: i < params.size then
let param := params[i]
let paramType ← inferType param
let instType? ← forallTelescopeReducing paramType fun xs _ => do
let type := mkAppN param xs
@ -67,8 +67,8 @@ private partial def mkSizeOfMotives (motiveFVars : Array Expr) (k : Array Expr
loop 0 #[]
where
loop (i : Nat) (motives : Array Expr) : MetaM α := do
if i < motiveFVars.size then
let type ← inferType motiveFVars[i]!
if h: i < motiveFVars.size then
let type ← inferType motiveFVars[i]
let motive ← forallTelescopeReducing type fun xs _ => do
mkLambdaFVars xs <| mkConst ``Nat
trace[Meta.sizeOf] "motive: {motive}"

4
src/Lean/Meta/Tactic/ElimInfo.lean
View file

@ -68,8 +68,8 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
| some targetPos => pure targetPos.val
let mut altsInfo := #[]
let env ← getEnv
for i in [:xs.size] do
let x := xs[i]!
for h: i in [:xs.size] do
let x := xs[i]
if x != motive && !targets.contains x then
let xDecl ← x.fvarId!.getDecl
if xDecl.binderInfo.isExplicit then

4
src/Lean/Meta/Tactic/Simp/Rewrite.lean
View file

@ -320,8 +320,8 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) :=
r ← mkCongrFun r argNew
unless modified do
return none
for i in [info.numDiscrs : args.size] do
let arg := args[i]!
for h: i in [info.numDiscrs : args.size] do
let arg := args[i]
r ← mkCongrFun r arg
return some r

16
src/Lean/PrettyPrinter/Delaborator/Builtins.lean
View file

@ -207,8 +207,8 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
`(⟨$[$(stx[1].getArgs)],*⟩)
let args := e.getAppArgs
let fieldVals := args.extract s.numParams args.size
for idx in [:fieldNames.size] do
let fieldName := fieldNames[idx]!
for h: idx in [:fieldNames.size] do
let fieldName := fieldNames[idx]
if (← getPPOption getPPStructureInstancesFlatten) && (Lean.isSubobjectField? env s.induct fieldName).isSome then
match stx[1][idx] with
| `({ $fields',* $[: $_]?}) =>
@ -397,9 +397,9 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
-- Field notation
if let some (fieldIdx, field) := field? then
if fieldIdx < args.size then
if h: fieldIdx < args.size then
let obj? : Option Term ← do
let arg := args[fieldIdx]!
let arg := args[fieldIdx]
if let .regular s := arg then
withNaryArg fieldIdx <| some <$> stripParentProjections s
else
@ -491,8 +491,8 @@ def useAppExplicit (numArgs : Nat) (paramKinds : Array ParamKind) : DelabM Bool
-- If there was an error collecting ParamKinds, fall back to explicit mode.
if paramKinds.size < numArgs then return true
if numArgs < paramKinds.size then
let nextParam := paramKinds[numArgs]!
if h: numArgs < paramKinds.size then
let nextParam := paramKinds[numArgs]
-- If the next parameter is implicit or inst implicit, fall back to explicit mode.
-- This is necessary for `@Eq` for example.
@ -741,8 +741,8 @@ where
m acc
usingNames {α} (varNames : Array Name) (x : DelabM α) (i : Nat := 0) : DelabM α :=
if i < varNames.size then
withBindingBody varNames[i]! <| usingNames varNames x (i+1)
if h: i < varNames.size then
withBindingBody varNames[i] <| usingNames varNames x (i+1)
else
x

4
src/Lean/Server/References.lean
View file

@ -312,8 +312,8 @@ where
findCanonicalRepresentative (idMap : Std.HashMap RefIdent RefIdent) (id : RefIdent) : RefIdent := Id.run do
let mut canonicalRepresentative := id
while idMap.contains canonicalRepresentative do
canonicalRepresentative := idMap[canonicalRepresentative]!
while h: idMap.contains canonicalRepresentative do
canonicalRepresentative := idMap[canonicalRepresentative]
return canonicalRepresentative
buildIdMap posMap := Id.run <| StateT.run' (s := Std.HashMap.empty) do