| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.
|
| |
|
|
|
|
|
|
|
|
| |
outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'.
Semantics of 'protected':
* The definition (i.e., body) of a 'protected' function is not visible outside the defining module
* The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions.
* In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected'
* The 'protected' status of a function must be preserved in refinement modules
|
| | |
|
| | |
|
| |
|
|
| |
their specifications (e.g., ensures clauses) are exported.
|
| |
|
|
|
|
| |
assumed.
Fixed cases where token was not being updated for refinement.
|
| | |
|
| | |
|
| |
|
|
| |
for special characters in identifiers
|
| |
|
|
| |
even if they are contained inside a split expression. Superposition is thought to be sound.
|
| |
|
|
| |
need to deal with unsplit expressions, like quantifiers)
|
| |
|
|
| |
the default module); these go into the (new) default class of each module
|
| | |
|
| |
|
Clément Pit--Claudel
leino
Unknown
Rustan Leino