diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index b5a2e5af13..d84ca8ae56 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -665,7 +665,7 @@ def isStringLit : Expr → Bool | _ => false def isCharLit (e : Expr) : Bool := - e.isAppOfArity `Char.ofNat 1 && e.appArg!.isNatLit + e.isAppOfArity ``Char.ofNat 1 && e.appArg!.isNatLit def constName! : Expr → Name | const n _ _ => n @@ -985,26 +985,26 @@ def etaExpandedStrict? : Expr → Option Expr | _ => none def getOptParamDefault? (e : Expr) : Option Expr := - if e.isAppOfArity `optParam 2 then + if e.isAppOfArity ``optParam 2 then some e.appArg! else none def getAutoParamTactic? (e : Expr) : Option Expr := - if e.isAppOfArity `autoParam 2 then + if e.isAppOfArity ``autoParam 2 then some e.appArg! else none @[export lean_is_out_param] def isOutParam (e : Expr) : Bool := - e.isAppOfArity `outParam 1 + e.isAppOfArity ``outParam 1 def isOptParam (e : Expr) : Bool := - e.isAppOfArity `optParam 2 + e.isAppOfArity ``optParam 2 def isAutoParam (e : Expr) : Bool := - e.isAppOfArity `autoParam 2 + e.isAppOfArity ``autoParam 2 @[export lean_expr_consume_type_annotations] partial def consumeTypeAnnotations (e : Expr) : Expr := diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 364e22e3a8..aec8cb7074 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -109,7 +109,7 @@ def isDefEqNat (s t : Expr) : MetaM LBool := do /-- Support for constraints of the form `("..." =?= String.mk cs)` -/ def isDefEqStringLit (s t : Expr) : MetaM LBool := do let isDefEq (s t) : MetaM LBool := toLBoolM <| Meta.isExprDefEqAux s t - if s.isStringLit && t.isAppOf `String.mk then + if s.isStringLit && t.isAppOf ``String.mk then isDefEq (toCtorIfLit s) t else if s.isAppOf `String.mk && t.isStringLit then isDefEq s (toCtorIfLit t) diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index b0fabbb106..388264ca96 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -622,8 +622,8 @@ def delabOfScientific : Delab := whenPPOption getPPCoercions do let Expr.lit (Literal.natVal m) _ ← pure (expr.getArg! 2) | failure let Expr.lit (Literal.natVal e) _ ← pure (expr.getArg! 4) | failure let s ← match expr.getArg! 3 with - | Expr.const `Bool.true _ _ => pure true - | Expr.const `Bool.false _ _ => pure false + | Expr.const ``Bool.true _ _ => pure true + | Expr.const ``Bool.false _ _ => pure false | _ => failure let str := toString m if s && e == str.length then @@ -728,7 +728,7 @@ def delabPSigma : Delab := delabSigmaCore (sigma := false) partial def delabDoElems : DelabM (List Syntax) := do let e ← getExpr - if e.isAppOfArity `Bind.bind 6 then + if e.isAppOfArity ``Bind.bind 6 then -- Bind.bind.{u, v} : {m : Type u → Type v} → [self : Bind m] → {α β : Type u} → m α → (α → m β) → m β let α := e.getAppArgs[2] let ma ← withAppFn $ withAppArg delab @@ -738,7 +738,7 @@ partial def delabDoElems : DelabM (List Syntax) := do withBindingBodyUnusedName fun n => do if body.hasLooseBVars then prependAndRec `(doElem|let $n:term ← $ma:term) - else if α.isConstOf `Unit || α.isConstOf `PUnit then + else if α.isConstOf ``Unit || α.isConstOf ``PUnit then prependAndRec `(doElem|$ma:term) else prependAndRec `(doElem|let _ ← $ma:term) @@ -754,13 +754,13 @@ partial def delabDoElems : DelabM (List Syntax) := do prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV) else let stx ← delab - return [←`(doElem|$stx:term)] + return [← `(doElem|$stx:term)] where prependAndRec x : DelabM _ := List.cons <$> x <*> delabDoElems @[builtinDelab app.Bind.bind] def delabDo : Delab := whenPPOption getPPNotation do - guard <| (← getExpr).isAppOfArity `Bind.bind 6 + guard <| (← getExpr).isAppOfArity ``Bind.bind 6 let elems ← delabDoElems let items ← elems.toArray.mapM (`(doSeqItem|$(·):doElem)) `(do $items:doSeqItem*) diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index b4ee6ec0f3..a11ffc84b2 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -231,7 +231,7 @@ def isFunLike (e : Expr) : MetaM Bool := do forallTelescopeReducing (← inferType e) fun xs b => return xs.size > 0 def isSubstLike (e : Expr) : Bool := - e.isAppOfArity `Eq.ndrec 6 || e.isAppOfArity `Eq.rec 6 + e.isAppOfArity ``Eq.ndrec 6 || e.isAppOfArity ``Eq.rec 6 def nameNotRoundtrippable (n : Name) : Bool := n.hasMacroScopes || isPrivateName n || containsNum n @@ -304,8 +304,8 @@ partial def isTrivialBottomUp (e : Expr) : AnalyzeM Bool := do let opts ← getOptions return e.isFVar || e.isConst || e.isMVar || e.isNatLit || e.isStringLit || e.isSort - || (getPPAnalyzeTrustOfNat opts && e.isAppOfArity `OfNat.ofNat 3) - || (getPPAnalyzeTrustOfScientific opts && e.isAppOfArity `OfScientific.ofScientific 5) + || (getPPAnalyzeTrustOfNat opts && e.isAppOfArity ``OfNat.ofNat 3) + || (getPPAnalyzeTrustOfScientific opts && e.isAppOfArity ``OfScientific.ofScientific 5) partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat := 10) : AnalyzeM Bool := do -- Here we check if `e` can be safely elaborated without its expected type. @@ -418,7 +418,7 @@ mutual let forceRegularApp : Bool := (getPPAnalyzeTrustSubst (← getOptions) && isSubstLike (← getExpr)) || (getPPAnalyzeTrustCoe (← getOptions) && isCoe (← getExpr)) - || (getPPAnalyzeTrustSubtypeMk (← getOptions) && (← getExpr).isAppOfArity `Subtype.mk 4) + || (getPPAnalyzeTrustSubtypeMk (← getOptions) && (← getExpr).isAppOfArity ``Subtype.mk 4) analyzeAppStagedCore { f, fType, args, mvars, bInfos, forceRegularApp } |>.run' { bottomUps := mkArray args.size false,