search

sdthompson1 / babylon

An experimental new programming language with verification features.
https://www.solarflare.org.uk/babylon
Other
0 stars 0 forks source link

Syntax review #5

Open sdthompson1 opened 1 month ago

sdthompson1 commented 1 month ago

Placeholder

sdthompson1 commented 2 weeks ago

Tyargs in patterns are currently parsed but ignored, e.g. case Just<i32>(x) => ... This could be misleading in case x isn't actually i32. Perhaps we should just forbid tyargs in that situation for now.

sdthompson1 commented 2 weeks ago

Maybe "uninterpreted" ghost functions (as in ghost f(): i32; with no body) should be allowed to have preconditions? (They are not allowed to have postconditions, on the grounds that this could introduce inconsistency, but I don't think there would be any problem with preconditions.)