Juliano Cardoso / circusRefine

taticaExtendVarScope.tex 525 Bytes
edit raw blame history 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
/* Tatica extendVarScope */

\tbegin
\ttactic extendVarScope()  \def


\tappliesto (AIn \circseq (\circmu X \circspot (\circvar d : \nat \circspot  A) \circseq EC))
        \tdo
            (\tskip \semibox(
							(\mubox (\tlaw Sequence_Unit_part_2() \tsemi \tlaw var_exp_seq() \tsemi \varbox (\tlaw Sequence_Unit_part_2() )))
							\tsemi \tlaw Var_Exp_Rec() \tsemi \tlaw Sequence_Unit_part_1()))
							\tsemi \tlaw var_exp_seq() \tsemi \varbox (\tskip \semibox \tlaw Sequence_Unit_part_1())
\tend