June 5th, 2017

Gen.Turgidson

Синтаксическое

В why3 можно писать условия навроде

0 <= i < j < n

Значат они именно то что можно подумать, никаких проблем с синтаксическим анализом вроде бы не создают и довольно удобочитаемы;

0 <= i && i < j && j < n

ничем кроме более длинной записи вроде как не лучше.

интересно почему идея не очень пошла в массы?