chore: enforce naming convention

library/Init/Lean/Expr.lean

@@ -231,38 +231,38 @@ def isAppOfArity : Expr → Name → Nat → Bool
 | app f _,   n, a+1 => isAppOfArity f n a
 | _,         _, _   => false
 
-def constName : Expr → Name
+def constName! : Expr → Name
 | const n _ => n
 | _         => panic! "constant expected"
 
-def constLevels : Expr → List Level
+def constLevels! : Expr → List Level
 | const _ ls => ls
 | _          => panic! "constant expected"
 
-def bvarIdx : Expr → Nat
+def bvarIdx! : Expr → Nat
 | bvar idx => idx
 | _        => panic! "bvar expected"
 
-def fvarName : Expr → Name
+def fvarName! : Expr → Name
 | fvar n => n
 | _      => panic! "fvar expected"
 
-def bindingName : Expr → Name
+def bindingName! : Expr → Name
 | forallE n _ _ _ => n
 | lam n _ _ _     => n
 | _               => panic! "binding expected"
 
-def bindingDomain : Expr → Expr
+def bindingDomain! : Expr → Expr
 | forallE _ _ d _ => d
 | lam _ _ d _     => d
 | _               => panic! "binding expected"
 
-def bindingBody : Expr → Expr
+def bindingBody! : Expr → Expr
 | forallE _ _ _ b => b
 | lam _ _ _ b     => b
 | _               => panic! "binding expected"
 
-def letName : Expr → Name
+def letName! : Expr → Name
 | letE n _ _ _ => n
 | _            => panic! "let expression expected"
 
@@ -404,7 +404,7 @@ match e with
 
 @[extern "lean_expr_update_const"]
 def updateConst (e : Expr) (newLevels : List Level) (h : e.isConst = true) : Expr :=
-const e.constName newLevels
+const e.constName! newLevels
 
 @[inline] def updateConst! (e : Expr) (newLevels : List Level) : Expr :=
 match e with
@@ -444,7 +444,7 @@ match e with
 
 @[extern "lean_expr_update_forall"]
 def updateForall (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isForall = true) : Expr :=
-forallE e.bindingName newBinfo newDomain newBody
+forallE e.bindingName! newBinfo newDomain newBody
 
 @[inline] def updateForall! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr :=
 match e with
@@ -458,7 +458,7 @@ match e with
 
 @[extern "lean_expr_update_lambda"]
 def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isLambda = true) : Expr :=
-lam e.bindingName newBinfo newDomain newBody
+lam e.bindingName! newBinfo newDomain newBody
 
 @[inline] def updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr :=
 match e with
@@ -472,7 +472,7 @@ match e with
 
 @[extern "lean_expr_update_let"]
 def updateLet (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (h : e.isLet = true) : Expr :=
-letE e.letName newType newVal newBody
+letE e.letName! newType newVal newBody
 
 @[inline] def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
 match e with

library/Init/Lean/TypeClass/Context.lean

@@ -184,7 +184,7 @@ partial def uInstantiate (ctx : Context) : Level → Level
 
 def eHasTmpMVar (e : Expr) : Bool :=
 if e.hasMVar
-then eFind (λ t => eIsMeta t || (t.isConst && t.constLevels.any uHasTmpMVar)) e
+then eFind (λ t => eIsMeta t || (t.isConst && t.constLevels!.any uHasTmpMVar)) e
 else false
 
 partial def slowWhnfApp (args : Array Expr) : Expr → Nat → Expr
@@ -211,18 +211,18 @@ partial def eUnify : Expr → Expr → EState String Context Unit
     e₂ ← slowWhnf <$> (EState.fromState $ eShallowInstantiate e₂);
     if e₁.isMVar && e₂.isMVar && e₁ == e₂ then pure ()
     else if eIsMeta e₂ && !(eIsMeta e₁) then eUnify e₂ e₁
-    else if e₁.isBVar && e₂.isBVar && e₁.bvarIdx == e₂.bvarIdx then pure ()
-    else if e₁.isFVar && e₂.isFVar && e₁.fvarName == e₂.fvarName then pure ()
-    else if e₁.isConst && e₂.isConst && e₁.constName == e₂.constName then
-      List.forM₂ uUnify e₁.constLevels e₂.constLevels
+    else if e₁.isBVar && e₂.isBVar && e₁.bvarIdx! == e₂.bvarIdx! then pure ()
+    else if e₁.isFVar && e₂.isFVar && e₁.fvarName! == e₂.fvarName! then pure ()
+    else if e₁.isConst && e₂.isConst && e₁.constName! == e₂.constName! then
+      List.forM₂ uUnify e₁.constLevels! e₂.constLevels!
     else if e₁.isApp && e₂.isApp && e₁.getAppNumArgs == e₂.getAppNumArgs then do
       let args₁ := e₁.getAppArgs;
       let args₂ := e₂.getAppArgs;
       eUnify e₁.getAppFn e₂.getAppFn;
       args₁.size.forM $ fun i => eUnify (args₁.get! i) (args₂.get! i)
     else if e₁.isForall && e₂.isForall then do
-      eUnify e₁.bindingDomain e₂.bindingDomain;
-      eUnify e₁.bindingBody e₂.bindingBody
+      eUnify e₁.bindingDomain! e₂.bindingDomain!;
+      eUnify e₁.bindingBody! e₂.bindingBody!
     else if eIsMeta e₁ && !(eOccursIn e₂ e₁) then
       match eMetaIdx e₁ with
       | some idx => EState.fromState $ eAssignIdx idx e₂

library/Init/Lean/TypeClass/Synth.lean

@@ -85,7 +85,7 @@ def quickIsClass (env : Environment) : Expr → Option (Option Name)
 | Expr.forallE _ _ _ b => quickIsClass b
 | Expr.app e _         =>
   let f := e.getAppFn;
-  if f.isConst && isClass env f.constName then some (some f.constName)
+  if f.isConst && isClass env f.constName! then some (some f.constName!)
   else if f.isLambda then none
   else some none
 | _            => some none
@@ -268,19 +268,19 @@ def collectEReplacements (env : Environment) (lctx : LocalContext) (locals : Arr
 | _, arg::args, _, _, _ => panic! "TODO(dselsam): this case not yet handled"
 
 def preprocessForOutParams (env : Environment) (goalType : Expr) : Context × Expr × Array (Level × Level) × Array (Expr × Expr) :=
-if !goalType.hasMVar && goalType.getAppFn.isConst && !hasOutParams env goalType.getAppFn.constName
+if !goalType.hasMVar && goalType.getAppFn.isConst && !hasOutParams env goalType.getAppFn.constName!
 then ({}, goalType, #[], #[])
 else
   let ⟨lctx, bodyGoalType, locals⟩ := introduceLocals 0 {} #[] goalType;
   let f := goalType.getAppFn;
   let fArgs := goalType.getAppArgs;
-  if !(f.isConst && isClass env f.constName)
+  if !(f.isConst && isClass env f.constName!)
   then ({}, goalType, #[], #[])
   else
-    let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels {} #[] #[];
-    let f := if uReplacements.isEmpty then f else Expr.const f.constName CLevels.toList;
+    let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels! {} #[] #[];
+    let f := if uReplacements.isEmpty then f else Expr.const f.constName! CLevels.toList;
     let fType :=
-      match env.find f.constName with
+      match env.find f.constName! with
       | none => panic! "found constant not in the environment"
       | some cInfo => cInfo.instantiateTypeUnivParams CLevels.toList;
     let (ctx, eReplacements, fArgs) := collectEReplacements env lctx locals fType fArgs.toList ctx #[] #[]; -- TODO: avoid fArgs.toList