This test shows one of the few cases were Matita is able to infer a dependent

[helm.git] / matita / library / assembly / vm.ma

diff --git a/matita/library/assembly/vm.ma b/matita/library/assembly/vm.ma
index 162b5df0f378cf8f28e096b56a02feba9fbe481f..30d073144c486c8040f37d170f09673490cab525 100644 (file)
--- a/matita/library/assembly/vm.ma
+++ b/matita/library/assembly/vm.ma
@@ -111,12 +111,31 @@ record status : Type ≝ {
   clk : nat
 }.
 
+notation "{hvbox('Acc' ≝ acc ; break 'Pc' ≝ pc ; break 'Spc' ≝ spc ; break 'Fz' ≝ fz ; break 'Fc' ≝ fc ; break  'M' ≝ m ; break 'Clk' ≝ clk)}"
+non associative with precedence 80 for
+ @{ 'mkstatus $acc $pc $spc $fz $fc $m $clk }.
+ 
+interpretation "mk_status" 'mkstatus acc pc spc fz fc m clk =
+ (cic:/matita/assembly/vm/status.ind#xpointer(1/1/1) acc pc spc fz fc m clk).
+
 definition update ≝
  λf: addr → byte.λa.λv.λx.
   match eqb x a with
    [ true ⇒ v
    | false ⇒ f x ].
 
+notation "hvbox(m break {a ↦ break v})" non associative with precedence 80 for 
+ @{ 'update $m $a $v }.
+ 
+notation "hvbox(m break {a ↦ break v} \nbsp x)" non associative with precedence 80 for 
+ @{ 'update4 $m $a $v $x }.
+ 
+interpretation "update" 'update m a v =
+  (cic:/matita/assembly/vm/update.con m a v).
+
+interpretation "update4" 'update4 m a v x =
+  (cic:/matita/assembly/vm/update.con m a v x).
+
 lemma update_update_a_a:
  ∀s,a,v1,v2,b.
   update (update s a v1) a v2 b = update s a v2 b.