Skip to content

proved the equivalence between realPoly$evalPoly and poly$poly

Mohit Tekriwal requested to merge polyProofs_semantics_relate into master

We relate the polynomial evaluation between what's defined in HOL4 and what's defined in realPolyScript.

[ PS: Earlier, I pushed the modified file to another branch which had a half baked definition of checkerProofs. So, I created a separate branch, since the pipeline failed once on that branch ]

Merge request reports