next up previous contents index
Next: Lemma Support Up: Rewriting Previous: Conversionals

Applying Conversions

 

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

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

RWT RewriteType
 

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

 



Karla Consroe
Wed Oct 23 13:48:45 EDT 1996