Commit 4267935b authored by charguer's avatar charguer

ok

parent 8fd9621d
......@@ -30,7 +30,7 @@ Implicit Types n : int.
Definition val_incr :=
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := val_add 'n 1 in
Let 'm := 'n '+ 1 in
val_set 'p 'm.
*)
......@@ -187,7 +187,7 @@ Proof using. intros. xapps. hsimpl~. Qed.
Definition val_decr :=
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := val_sub 'n 1 in
Let 'm := 'n '- 1 in
val_set 'p 'm.
Lemma rule_decr : forall p n,
......
......@@ -264,7 +264,7 @@ Hint Extern 1 (Register_Spec val_mlist_copy) => Provide Rule_mlist_copy.
Definition val_mlist_length : val :=
ValFix 'f 'p :=
If_ val_neq 'p null Then (
If_ 'p '<> null Then (
Let 'q := val_get_tl 'p in
Let 'n := 'f 'q in
val_add 'n 1
......@@ -353,7 +353,7 @@ Qed.
Definition val_mlist_iter : val :=
ValFix 'g 'f 'p :=
If_ val_neq 'p null Then
If_ 'p '<> null Then
Let 'x := val_get_hd 'p in
'f 'x ;;
Let 'q := val_get_tl 'p in
......@@ -446,7 +446,7 @@ Definition val_mlist_length_loop : val :=
Let 'r := val_ref 'p1 in
Let 'n := val_ref 0 in
While (Let 'p := val_get 'r in
val_neq 'p null) Do
'p '<> null) Do
val_incr 'n ;;
Let 'p := val_get 'r in
Let 'q := val_get_tl 'p in
......@@ -487,9 +487,9 @@ Qed.
Definition val_mlist_incr : val :=
ValFix 'f 'p :=
If_ val_neq 'p null Then (
If_ 'p '<> null Then (
Let 'x := val_get_hd 'p in
Let 'y := val_add 'x 1 in
Let 'y := 'x '+ 1 in
val_set_hd 'p 'y;;
Let 'q := val_get_tl 'p in
'f 'q
......@@ -517,7 +517,7 @@ Definition val_mlist_in_place_rev : val :=
Let 'r := val_ref 'p1 in
Let 's := val_ref null in
While (Let 'p := val_get 'r in
val_neq 'p null) Do
'p '<> null) Do
Let 'p := val_get 'r in
Let 'q := val_get_tl 'p in
val_set 'r 'q ;;
......
......@@ -315,10 +315,10 @@ Global Opaque MList.
Definition val_mlist_length : val :=
ValFix 'f 'p :=
If_ val_neq 'p null Then (
If_ 'p '<> null Then (
Let 'q := val_get_tl 'p in
Let 'n := 'f 'q in
val_add 'n 1
'n '+ 1
) Else (
0
).
......@@ -440,7 +440,7 @@ Definition val_mlist_length_loop : val :=
Let 'r := val_ref 'p1 in
Let 'n := val_ref 0 in
While (Let 'p := val_get 'r in
val_neq 'p null) Do
'p '<> null) Do
val_incr 'n ;;
Let 'p := val_get 'r in
Let 'q := val_get_tl 'p in
......
......@@ -395,7 +395,7 @@ Hint Extern 1 (Register_spec val_root) => Provide rule_root.
Definition val_compress :=
ValFun 'p 'x 'z :=
LetFix 'f 'x :=
If_ val_neq 'x 'z Then
If_ 'x '<> 'z Then
Let 'y := val_array_get 'p 'x in
val_array_set 'p 'x 'z ;;
'f 'y
......@@ -470,7 +470,7 @@ Definition val_union :=
ValFun 'p 'x 'y :=
Let 'r := val_find 'p 'x in
Let 's := val_find 'p 'y in
If_ val_neq 'r 's Then
If_ 'r '<> 's Then
val_array_set 'p 'r 's
End.
......
......@@ -81,6 +81,10 @@ Definition val_neq :=
Let 'x := ('m '= 'n) in
val_not 'x.
Notation "t1 '<> t2" :=
(val_neq t1 t2)
(at level 69) : trm_scope.
Lemma rule_neq : forall v1 v2,
triple (val_neq v1 v2)
\[]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment