Rodin Handbook





 

4.3.4 I’ve added a witness for Xyz but it keeps saying “Identifier Xyz has not been defined”

As specified in the Section 3.2.4.4.4, the witness must be labelled with the name Xyz of the abstract parameter of the event that is being refined. A concrete example can be found in Section 2.8.5.