From 1f000feb8035dcee175e649ca32e6dd538a46889 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 24 May 2025 09:00:37 +0200 Subject: [PATCH] chore: remove unnecessary `partial` in Lean.Expr (#8464) The termination prover has gotten stronger since these definitions were written, and now they can be proved terminating automatically. (One definition had to be changed slightly because it wasn't actually terminating before.) --- src/Lean/Expr.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index eb8e6c626e..bc394c314d 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -750,7 +750,7 @@ def mkStrLit (s : String) : Expr := def mkAppN (f : Expr) (args : Array Expr) : Expr := args.foldl mkApp f -private partial def mkAppRangeAux (n : Nat) (args : Array Expr) (i : Nat) (e : Expr) : Expr := +private def mkAppRangeAux (n : Nat) (args : Array Expr) (i : Nat) (e : Expr) : Expr := if i < n then mkAppRangeAux n args (i+1) (mkApp e args[i]!) else e /-- `mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ]` ==> the expression `f a_i ... a_{j-1}` -/ @@ -1502,8 +1502,8 @@ abbrev PersistentExprStructMap (α : Type) := PHashMap ExprStructEq α namespace Expr -private partial def mkAppRevRangeAux (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : Expr := - if i == start then b +private def mkAppRevRangeAux (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : Expr := + if i ≤ start then b else let i := i - 1 mkAppRevRangeAux revArgs start (mkApp b revArgs[i]!) i @@ -1880,7 +1880,7 @@ def updateFn : Expr → Expr → Expr /-- Eta reduction. If `e` is of the form `(fun x => f x)`, then return `f`. -/ -partial def eta (e : Expr) : Expr := +def eta (e : Expr) : Expr := match e with | Expr.lam _ d b _ => let b' := b.eta