Applying Conversions

Rewrite (c:convn) (i:int) : tactic

Apply conversion c to clause i. The subgoal with the result of the conversion is always labelled main. The rest have various labels that all fall into the aux subgoal label class.

RW Rewrite
  RWH c RW (HigherC c)
  RWU c RW (SweepUpC c)
  RWD c RW (SweepDnC c)
  RWN n c RW (NthC n c)
  RWAddr addr c RW (AddrC addr c)
 

RewriteType (c:convn) (i:int) : tactic

Apply   c to type of member or equality term in clause i. The subgoal with the result of the conversion is always labelled main. The rest have various labels that all fall into the aux subgoal label class. The advantage of this tactic over the usual Rewrite is that this generates simpler well-formedness goals. In particular, this tactic generates no well-formedness goals involving the equands of the equality or the element of the member term.

RWT RewriteType
 

apply_conv (c:convn) (t:term) : term

apply_conv evaluates a conversion with an empty environment. It is very useful for testing conversions.