Rodin Handbook





 
Previous: Witness for Xyz missing. Default witness generated Up: Modeling Next: In INITIALISATION, I get Witness Xyz must be a disappearing abstract variable or parameter User Manual for Rodin v.2.3

Feedback

4.3.2 Identifier Xyz should not occur free in a witness

You refer to Xyz in a witness predicate where Xyz is a disappearing abstract variable or parameter which is not set as the witness label.

Previous: Witness for Xyz missing. Default witness generated Up: Modeling Next: In INITIALISATION, I get Witness Xyz must be a disappearing abstract variable or parameter  
User Manual for Rodin v.2.3 : Frequently Asked Questions : Modeling : Identifier Xyz should not occur free in a witness