Commit 251ab0d5 authored by Robbert Krebbers's avatar Robbert Krebbers

Turn some -> arrows into →.

parent d27b81ff
......@@ -443,7 +443,7 @@ End cmra_monotone.
(** Functors *)
Structure rFunctor := RFunctor {
rFunctor_car : cofeT cofeT -> cmraT;
rFunctor_car : cofeT cofeT cmraT;
rFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
rFunctor_ne A1 A2 B1 B2 n :
......
......@@ -340,7 +340,7 @@ Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
(** Functors *)
Structure cFunctor := CFunctor {
cFunctor_car : cofeT cofeT -> cofeT;
cFunctor_car : cofeT cofeT cofeT;
cFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
cFunctor_ne {A1 A2 B1 B2} n :
......
......@@ -91,8 +91,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.
Notation "p .1" := (fst p) (at level 10, format "p .1").
Notation "p .2" := (snd p) (at level 10, format "p .2").
Definition fun_map {A A' B B'} (f : A' -> A) (g : B -> B')
(h : A -> B) : A' -> B' := g h f.
Definition fun_map {A A' B B'} (f : A' A) (g : B B')
(h : A B) : A' B' := g h f.
Definition prod_map {A A' B B'} (f : A A') (g : B B')
(p : A * B) : A' * B' := (f (p.1), g (p.2)).
Arguments prod_map {_ _ _ _} _ _ !_ /.
......
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