Skip to content
Snippets Groups Projects
Commit a0708918 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix indentation

parent 3e0ca8c7
No related branches found
No related tags found
1 merge request!19Mclaurin series and first checker implementation with soundness
Pipeline #52603 passed
......@@ -93,7 +93,7 @@ Definition validateZeroesLeqErr_def:
abs (poly diffPoly (SND iv)) ub + B * e
validBounds iv zeroes
EVERY (λ (u,v). poly (diff diffPoly) u * poly (diff diffPoly) v 0) zeroes
recordered (FST iv) zeroes (SND iv))
recordered (FST iv) zeroes (SND iv))
then
isValid (ub + B * e eps) "Bounding error too large"
else Invalid "Outer points bigger than error"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment