max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: inverse rhs construction order in BEq's handler

Browse source
This commit is contained in:
arthur-adjedj 2024-03-27 17:56:51 +01:00 • committed by Kim Morrison
parent f830fc9f4d
commit 7253ef8751
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/Elab/Deriving/BEq.lean
View file

@ -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)