Rodin Handbook





 

4.3.1 Witness for Xyz missing. Default witness generated

A parameter has disappeared during a refinement. If this is intentional, add a witness (3.2.4.4.4) to tell the machine how the abstract parameter should refined.