Rodin Handbook
This work is sponsored by the Deploy Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
User Manual for Rodin v.2.3 |  |
 |
 |
4.3.1 Witness for Xyz missing. Default witness generated
A parameter has disappeared during a refinement. If this is intentional, you have to add a witness 3.2.3.4.4 telling how the abstract parameter is refined.
|
|
|
|
|
|