search

Twigonometry / IsabelleDSL

IsabelleDSL (iDSL) is a framework for generating Domain-Specific Languages from specifications written in Isabelle
0 stars 0 forks source link

Fix non-integer clash in Calculator #19

Open Twigonometry opened 2 years ago

Twigonometry commented 2 years ago

Currently calculator only processes integers, but Python implicitly uses floats. Either switch to Python integer division only, or allow reals in isabelle spec.

It's fine not to fix this - it serves as a good example of where the testing suite can catch an error in the model.