Rodin Handbook
This work is sponsored by the Deploy Project
This work is sponsored by the ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
Rodin User’s Handbook v.2.8 |  |
 |
 |
4.3.2 Identifier Xyz should not occur free in a witness
This means that the Xyz identifier appears in a witness predicate, but Xyz is a disappearing abstract variable or parameter and is not set as the witness label. To resolve this error, set change the witness label to the identifier Xyz.
|
|
|
|
|
|