Whiley / RFCs

Request for Comment (RFC) proposals for substantial changes to the Whiley language.
3 stars 2 forks source link

Exponent Operator #91

Open DavePearce opened 3 years ago

DavePearce commented 3 years ago

(originally suggested by @utting)

It would be helpful to have an explicit exponent operator, in particular to help with verification. The usual syntax for such an operator is x**y. A few points:

  1. Does Boogie support an exponent operator? I'm not sure. Doesn't look like Dafny does.