chore: use let_expr to cleanup code

src/Lean/Elab/StructInst.lean

@@ -802,10 +802,8 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex
         let arg ← mkFreshExprMVar d
         mkDefaultValueAux? struct (b.instantiate1 arg)
   | e =>
-    if e.isAppOfArity ``id 2 then
-      return some e.appArg!
-    else
-      return some e
+    let_expr id _ a := e | return some e
+    return some a
 
 def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
   withRef struct.ref do

src/Lean/Expr.lean

@@ -1075,33 +1075,6 @@ def isAppOfArity' : Expr → Name → Nat → Bool
   | app f _,    n, a+1 => isAppOfArity' f n a
   | _,          _,  _   => false
 
-/--
-Checks if an expression is a "natural number numeral in normal form",
-i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`
-where `n` matches `.lit (.natVal n)` for some literal natural number `n`.
-and if so returns `n`.
--/
--- Note that `Expr.lit (.natVal n)` is not considered in normal form!
-def nat? (e : Expr) : Option Nat := do
-  guard <| e.isAppOfArity ``OfNat.ofNat 3
-  let lit (.natVal n) := e.appFn!.appArg! | none
-  n
-
-/--
-Checks if an expression is an "integer numeral in normal form",
-i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
-or the negation of a positive natural number numberal in normal form,
-and if so returns the integer.
--/
-def int? (e : Expr) : Option Int :=
-  if e.isAppOfArity ``Neg.neg 3 then
-    match e.appArg!.nat? with
-    | none => none
-    | some 0 => none
-    | some n => some (-n)
-  else
-    e.nat?
-
 private def getAppNumArgsAux : Expr → Nat → Nat
   | app f _, n => getAppNumArgsAux f (n+1)
   | _,       n => n
@@ -1638,6 +1611,31 @@ def isFalse (e : Expr) : Bool :=
 def isTrue (e : Expr) : Bool :=
   e.cleanupAnnotations.isConstOf ``True
 
+/--
+Checks if an expression is a "natural number numeral in normal form",
+i.e. of type `Nat`, and explicitly of the form `OfNat.ofNat n`
+where `n` matches `.lit (.natVal n)` for some literal natural number `n`.
+and if so returns `n`.
+-/
+-- Note that `Expr.lit (.natVal n)` is not considered in normal form!
+def nat? (e : Expr) : Option Nat := do
+  let_expr OfNat.ofNat _ n _ := e | failure
+  let lit (.natVal n) := n | failure
+  n
+
+/--
+Checks if an expression is an "integer numeral in normal form",
+i.e. of type `Nat` or `Int`, and either a natural number numeral in normal form (as specified by `nat?`),
+or the negation of a positive natural number numberal in normal form,
+and if so returns the integer.
+-/
+def int? (e : Expr) : Option Int :=
+  let_expr Neg.neg _ _ a := e | e.nat?
+  match a.nat? with
+  | none => none
+  | some 0 => none
+  | some n => some (-n)
+
 /-- Return true iff `e` contains a free variable which satisfies `p`. -/
 @[inline] def hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool :=
   let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else

src/Lean/Meta/Injective.lean

@@ -26,10 +26,8 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
 
 def elimOptParam (type : Expr) : CoreM Expr := do
   Core.transform type fun e =>
-    if e.isAppOfArity  ``optParam 2 then
-      return TransformStep.visit (e.getArg! 0)
-    else
-      return .continue
+    let_expr optParam _ a := e | return .continue
+    return TransformStep.visit a
 
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam

src/Lean/Meta/LitValues.lean

@@ -27,11 +27,10 @@ def getRawNatValue? (e : Expr) : Option Nat :=
 
 /-- Return `some (n, type)` if `e` is an `OfNat.ofNat`-application encoding `n` for a type with name `typeDeclName`. -/
 def getOfNatValue? (e : Expr) (typeDeclName : Name) : MetaM (Option (Nat × Expr)) := OptionT.run do
-  let e := e.consumeMData
-  guard <| e.isAppOfArity' ``OfNat.ofNat 3
-  let type ← whnfD (e.getArg!' 0)
+  let_expr OfNat.ofNat type n _ ← e | failure
+  let type ← whnfD type
   guard <| type.getAppFn.isConstOf typeDeclName
-  let .lit (.natVal n) := (e.getArg!' 1).consumeMData | failure
+  let .lit (.natVal n) := n.consumeMData | failure
   return (n, type)
 
 /-- Return `some n` if `e` is a raw natural number or an `OfNat.ofNat`-application encoding `n`. -/
@@ -46,16 +45,15 @@ def getNatValue? (e : Expr) : MetaM (Option Nat) := do
 def getIntValue? (e : Expr) : MetaM (Option Int) := do
   if let some (n, _) ← getOfNatValue? e ``Int then
     return some n
-  if e.isAppOfArity' ``Neg.neg 3 then
-    let some (n, _) ← getOfNatValue? (e.getArg!' 2) ``Int | return none
-    return some (-n)
-  return none
+  let_expr Neg.neg _ _ a ← e | return none
+  let some (n, _) ← getOfNatValue? a ``Int | return none
+  return some (-↑n)
 
 /-- Return `some c` if `e` is a `Char.ofNat`-application encoding character `c`. -/
-def getCharValue? (e : Expr) : MetaM (Option Char) := OptionT.run do
-  guard <| e.isAppOfArity' ``Char.ofNat 1
-  let n ← getNatValue? (e.getArg!' 0)
-  return Char.ofNat n
+def getCharValue? (e : Expr) : MetaM (Option Char) := do
+  let_expr Char.ofNat n ← e | return none
+  let some n ← getNatValue? n | return none
+  return some (Char.ofNat n)
 
 /-- Return `some s` if `e` is of the form `.lit (.strVal s)`. -/
 def getStringValue? (e : Expr) : (Option String) :=

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -162,42 +162,42 @@ builtin_simproc [simp, seval] reduceRotateRight (BitVec.rotateRight _ _) :=
 
 /-- Simplification procedure for append on `BitVec`. -/
 builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
-  unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
-  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
-  let some v₂ ← fromExpr? e.appArg! | return .continue
+  let_expr HAppend.hAppend _ _ _ _ a b ← e | return .continue
+  let some v₁ ← fromExpr? a | return .continue
+  let some v₂ ← fromExpr? b | return .continue
   return .done { expr := toExpr (v₁.value ++ v₂.value) }
 
 /-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
 builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
-  unless e.isAppOfArity ``cast 4 do return .continue
-  let some v ← fromExpr? e.appArg! | return .continue
-  let some m ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let_expr cast _ m _ v ← e | return .continue
+  let some v ← fromExpr? v | return .continue
+  let some m ← Nat.fromExpr? m | return .continue
   return .done { expr := toExpr (BitVec.ofNat m v.value.toNat) }
 
 /-- Simplification procedure for `BitVec.toNat`. -/
 builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
-  unless e.isAppOfArity ``BitVec.toNat 2 do return .continue
-  let some v ← fromExpr? e.appArg! | return .continue
+  let_expr BitVec.toNat _ v ← e | return .continue
+  let some v ← fromExpr? v | return .continue
   return .done { expr := mkNatLit v.value.toNat }
 
 /-- Simplification procedure for `BitVec.toInt`. -/
 builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
-  unless e.isAppOfArity ``BitVec.toInt 2 do return .continue
-  let some v ← fromExpr? e.appArg! | return .continue
+  let_expr BitVec.toInt _ v ← e | return .continue
+  let some v ← fromExpr? v | return .continue
   return .done { expr := toExpr v.value.toInt }
 
 /-- Simplification procedure for `BitVec.ofInt`. -/
 builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
-  unless e.isAppOfArity ``BitVec.ofInt 2 do return .continue
-  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  let some i ← Int.fromExpr? e.appArg! | return .continue
+  let_expr BitVec.ofInt n i ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
+  let some i ← Int.fromExpr? i | return .continue
   return .done { expr := toExpr (BitVec.ofInt n i) }
 
 /-- Simplification procedure for ensuring `BitVec.ofNat` literals are normalized. -/
 builtin_simproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
-  unless e.isAppOfArity ``BitVec.ofNat 2 do return .continue
-  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  let some v ← Nat.fromExpr? e.appArg! | return .continue
+  let_expr BitVec.ofNat n v ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
+  let some v ← Nat.fromExpr? v | return .continue
   let bv := BitVec.ofNat n v
   if bv.toNat == v then return .continue -- already normalized
   return .done { expr := toExpr (BitVec.ofNat n v) }
@@ -226,9 +226,9 @@ builtin_simproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
 
 /-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
-  unless e.isAppOfArity ``zeroExtend' 4 do return .continue
-  let some v ← fromExpr? e.appArg! | return .continue
-  let some w ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let_expr zeroExtend' _ w _ v ← e | return .continue
+  let some v ← fromExpr? v | return .continue
+  let some w ← Nat.fromExpr? w | return .continue
   if h : v.n ≤ w then
     return .done { expr := toExpr (v.value.zeroExtend' h) }
   else
@@ -236,25 +236,25 @@ builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
 
 /-- Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _) := fun e => do
-  unless e.isAppOfArity ``shiftLeftZeroExtend 3 do return .continue
-  let some v ← fromExpr? e.appFn!.appArg! | return .continue
-  let some m ← Nat.fromExpr? e.appArg! | return .continue
+  let_expr shiftLeftZeroExtend _ v m ← e | return .continue
+  let some v ← fromExpr? v | return .continue
+  let some m ← Nat.fromExpr? m | return .continue
   return .done { expr := toExpr (v.value.shiftLeftZeroExtend m) }
 
 /-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
-  unless e.isAppOfArity ``extractLsb' 4 do return .continue
-  let some v ← fromExpr? e.appArg! | return .continue
-  let some start ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
-  let some len ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let_expr extractLsb' _ start len v ← e | return .continue
+  let some v ← fromExpr? v | return .continue
+  let some start ← Nat.fromExpr? start | return .continue
+  let some len ← Nat.fromExpr? len | return .continue
   return .done { expr := toExpr (v.value.extractLsb' start len) }
 
 /-- Simplification procedure for `replicate` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
-  unless e.isAppOfArity ``replicate 3 do return .continue
-  let some v ← fromExpr? e.appArg! | return .continue
-  let some w ← Nat.fromExpr? e.appFn!.appArg! | return .continue
-  return .done { expr := toExpr (v.value.replicate w) }
+  let_expr replicate _ i v ← e | return .continue
+  let some v ← fromExpr? v | return .continue
+  let some i ← Nat.fromExpr? i | return .continue
+  return .done { expr := toExpr (v.value.replicate i) }
 
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
@@ -264,8 +264,8 @@ builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend
 
 /-- Simplification procedure for `allOnes` -/
 builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
-  unless e.isAppOfArity ``allOnes 1 do return .continue
-  let some n ← Nat.fromExpr? e.appArg! | return .continue
+  let_expr allOnes n ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
   return .done { expr := toExpr (allOnes n) }
 
 end BitVec

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -42,8 +42,8 @@ builtin_simproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Ch
 builtin_simproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum
 builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3
 builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
-  unless e.isAppOfArity ``Char.val 1 do return .continue
-  let some c ← fromExpr? e.appArg! | return .continue
+  let_expr Char.val arg ← e | return .continue
+  let some c ← fromExpr? arg | return .continue
   return .done { expr := toExpr c.val }
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
@@ -60,12 +60,12 @@ builtin_simproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do
   return .done { expr := e }
 
 builtin_simproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do
-  unless e.isAppOfArity ``Char.ofNatAux 2 do return .continue
-  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let_expr Char.ofNatAux n _ ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
   return .done { expr := toExpr (Char.ofNat n) }
 
 builtin_simproc [simp, seval] reduceDefault ((default : Char)) := fun e => do
-  unless e.isAppOfArity ``default 2 do return .continue
+  let_expr default _ _ ← e | return .continue
   return .done { expr := toExpr (default : Char) }
 
 end Char

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean

@@ -10,33 +10,29 @@ import Lean.Meta.Tactic.Simp.Simproc
 open Lean Meta Simp
 
 builtin_simproc ↓ [simp, seval] reduceIte (ite _ _ _) := fun e => do
-  unless e.isAppOfArity ``ite 5 do return .continue
-  let c := e.getArg! 1
+  let_expr f@ite α c i tb eb ← e | return .continue
   let r ← simp c
   if r.expr.isTrue then
-    let eNew  := e.getArg! 3
-    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
-    return .visit { expr := eNew, proof? := pr }
+    let pr    := mkApp (mkApp5 (mkConst ``ite_cond_eq_true f.constLevels!) α c i tb eb) (← r.getProof)
+    return .visit { expr := tb, proof? := pr }
   if r.expr.isFalse then
-    let eNew  := e.getArg! 4
-    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
-    return .visit { expr := eNew, proof? := pr }
+    let pr    := mkApp (mkApp5 (mkConst ``ite_cond_eq_false f.constLevels!) α c i tb eb) (← r.getProof)
+    return .visit { expr := eb, proof? := pr }
   return .continue
 
 builtin_simproc ↓ [simp, seval] reduceDite (dite _ _ _) := fun e => do
-  unless e.isAppOfArity ``dite 5 do return .continue
-  let c := e.getArg! 1
+  let_expr f@dite α c i tb eb ← e | return .continue
   let r ← simp c
   if r.expr.isTrue then
     let pr    ← r.getProof
     let h     := mkApp2 (mkConst ``of_eq_true) c pr
-    let eNew  := mkApp (e.getArg! 3) h |>.headBeta
-    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) pr
+    let eNew  := mkApp tb h |>.headBeta
+    let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_true f.constLevels!) α c i tb eb) pr
     return .visit { expr := eNew, proof? := prNew }
   if r.expr.isFalse then
     let pr    ← r.getProof
     let h     := mkApp2 (mkConst ``of_eq_false) c pr
-    let eNew  := mkApp (e.getArg! 4) h |>.headBeta
-    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) pr
+    let eNew  := mkApp eb h |>.headBeta
+    let prNew := mkApp (mkApp5 (mkConst ``dite_cond_eq_false f.constLevels!) α c i tb eb) pr
     return .visit { expr := eNew, proof? := prNew }
   return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -57,7 +57,7 @@ builtin_simproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
 
 /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do
-  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
+  let_expr OfNat.ofNat _ _ _ ← e | return .continue
   return .done { expr := e }
 
 builtin_simproc [simp, seval] reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·)
@@ -67,9 +67,9 @@ builtin_simproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv
 builtin_simproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
 
 builtin_simproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
-  unless e.isAppOfArity ``HPow.hPow 6 do return .continue
-  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
-  let some v₂ ← Nat.fromExpr? e.appArg! | return .continue
+  let_expr HPow.hPow _ _ _ _ a b ← e | return .continue
+  let some v₁ ← fromExpr? a | return .continue
+  let some v₂ ← Nat.fromExpr? b | return .continue
   return .done { expr := toExpr (v₁ ^ v₂) }
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -65,7 +65,7 @@ builtin_simproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``
 
 /-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do
-  unless e.isAppOfArity ``OfNat.ofNat 3 do return .continue
+  let_expr OfNat.ofNat _ _ _ ← e | return .continue
   return .done { expr := e }
 
 end Nat