Closed mhk119 closed 10 months ago
Also, in smtRw
you could iterate through arrays instead of indices to avoid unsafe operations, like:
for innerArr in arr do
let m := innerArr.size
if m > 1 then
for j in [: m-1] do
let r ← mv'.rewrite (← mv'.getType) (mkAppN assoc #[innerArr[m-j-2]!]) true
mv' ← mv'.replaceTargetEq r.eNew r.eqProof
You could also iterate through the Expr
s in innerArr.reverse
instead of the indices.
It looks like you are always skipping the last element of each array? if j = 0
then m - j - 2 = m - 2
, whereas the last element is at position m - 1
This is looking good! Two comments about the last commit (please make a PR before pushing to main, so its easier to review):
- It's not necessary to do
replaceMainGoal [mv]
at the end ofevalSMTRw
. The goal is already closed when you domv'.refl
- The variable
m
inside both for-loops insmtRw
does not need to be mutable
Oh thanks. This is nicer.
Also, in
smtRw
you could iterate through arrays instead of indices to avoid unsafe operations, like:for innerArr in arr do let m := innerArr.size if m > 1 then for j in [: m-1] do let r ← mv'.rewrite (← mv'.getType) (mkAppN assoc #[innerArr[m-j-2]!]) true mv' ← mv'.replaceTargetEq r.eNew r.eqProof
You could also iterate through the
Expr
s ininnerArr.reverse
instead of the indices. It looks like you are always skipping the last element of each array? ifj = 0
thenm - j - 2 = m - 2
, whereas the last element is at positionm - 1
Yes. I am skipping the last element deliberately. This is also why I iterated over indices instead. I can try iterating through arrays though.
This is looking good! Two comments about the last commit (please make a PR before pushing to main, so its easier to review):
replaceMainGoal [mv]
at the end ofevalSMTRw
. The goal is already closed when you domv'.refl
m
inside both for-loops insmtRw
does not need to be mutable