This command is part of the experimental refinement editor.
The remove invariant command refines a specification statement to replace its invariant by true. It applies the following inference rule of the refinement calculus.
? P I ? Q I ? F[P, Q]
No code is implicitly generated by this refinement rule.
The remove invariant command is applicable when a specification statement F[P,I,Q] in a goal is inspected, except where I is already true.
"remove invariant" p
This example applies the remove invariant command to specification statement p.