From 7253ef8751f76bcbe0e6f46dcfa8069699a2bac7 Mon Sep 17 00:00:00 2001 From: arthur-adjedj Date: Wed, 27 Mar 2024 17:56:51 +0100 Subject: [PATCH] chore: inverse rhs construction order in `BEq`'s handler --- src/Lean/Elab/Deriving/BEq.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index c3c8c0b9f4..10d2fae20a 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -43,12 +43,8 @@ where let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] let mut rhs ← `(true) - -- add `_` for inductive parameters, they are inaccessible - for _ in [:indVal.numParams] do - ctorArgs1 := ctorArgs1.push (← `(_)) - ctorArgs2 := ctorArgs2.push (← `(_)) for i in [:ctorInfo.numFields] do - let x := xs[indVal.numParams + i]! + let x := xs[indVal.numParams + ctorInfo.numFields - i - 1]! if type.containsFVar x.fvarId! then -- If resulting type depends on this field, we don't need to compare ctorArgs1 := ctorArgs1.push (← `(_)) @@ -62,11 +58,15 @@ where if (← isProp xType) then continue if xType.isAppOf indVal.name then - rhs ← `($rhs && $(mkIdent auxFunName):ident $a:ident $b:ident) + rhs ← `($(mkIdent auxFunName):ident $a:ident $b:ident && $rhs) else - rhs ← `($rhs && $a:ident == $b:ident) - patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1:term*)) - patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs2:term*)) + rhs ← `($a:ident == $b:ident && $rhs) + -- add `_` for inductive parameters, they are inaccessible + for _ in [:indVal.numParams] do + ctorArgs1 := ctorArgs1.push (← `(_)) + ctorArgs2 := ctorArgs2.push (← `(_)) + patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1.reverse:term*)) + patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs2.reverse:term*)) `(matchAltExpr| | $[$patterns:term],* => $rhs:term) alts := alts.push alt alts := alts.push (← mkElseAlt)