non associative with precedence 80 for
@{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
- (cic:/matita/freescale/status/alu_HC05.ind#xpointer(1/1/1) acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
+ (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
(* ALU dell'HC08/HCS08 *)
record alu_HC08: Type ≝
non associative with precedence 80 for
@{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
- (cic:/matita/freescale/status/alu_HC08.ind#xpointer(1/1/1) acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
+ (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
(* ALU dell'RS08 *)
record alu_RS08: Type ≝
non associative with precedence 80 for
@{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
- (cic:/matita/freescale/status/alu_RS08.ind#xpointer(1/1/1) acclow pc pcm spc xm psm zfl cfl).
+ (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
(* tipo processore dipendente dalla mcu, varia solo la ALU *)
record any_status (mcu:mcu_type) (t:memory_impl): Type ≝
notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
for @{ 'mk_any_status $alu $mem $chk $clk }.
interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
- (cic:/matita/freescale/status/any_status.ind#xpointer(1/1/1) alu mem chk clk).
+ (mk_any_status alu mem chk clk).
(* **************** *)
(* GETTER SPECIFICI *)