Commit 17736977 authored by Robbert Krebbers's avatar Robbert Krebbers

Replace occurences of -> by →.

parent 4c93ce20
Pipeline #187 passed with stage
......@@ -54,7 +54,7 @@ Record CofeMixin A `{Equiv A, Compl A} := {
mixin_dist_S n x y : x {S n} y x {n} y;
mixin_conv_compl n c : compl c {n} c (S n)
}.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
Class Contractive `{Dist A, Dist B} (f : A B) :=
contractive n x y : ( i, i < n x {i} y) f x {n} f y.
(** Bundeled version *)
......
......@@ -85,7 +85,7 @@ Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
Proof. by split=> n x Hx. Qed.
Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
`{!CMRAMonotone f} `{!CMRAMonotone g}:
( x, f x g x) -> x, uPred_map f x uPred_map g x.
( x, f x g x) x, uPred_map f x uPred_map g x.
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 uPredC M2).
......
......@@ -11,7 +11,7 @@ Local Notation iProp := (iPropG heap_lang Σ).
(* TODO: Maybe notation for LocV (and Loc)? *)
Lemma barrier_spec (heapN N : namespace) :
heapN N
recv send : loc -> iProp -n> iProp,
recv send : loc iProp -n> iProp,
( P, heap_ctx heapN {{ True }} newchan '() {{ λ v, l, v = LocV l recv l P send l P }})
( l P, {{ send l P P }} signal (LocV l) {{ λ _, True }})
( l P, {{ recv l P }} wait (LocV l) {{ λ _, P }})
......
......@@ -183,7 +183,7 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
| _, _, _ => None
end.
Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
Inductive head_step : expr state expr state option expr Prop :=
| BetaS f x e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Rec f x e1) e2) σ
......
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