Commit 78ee4940 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/functor_record' into 'master'

Make functors a `Record` instead of a `Structure`.

See merge request iris/iris!256
parents 607933e0 bcac37c5
Pipeline #17085 failed with stage
in 0 seconds
...@@ -765,7 +765,7 @@ Section cmra_morphism. ...@@ -765,7 +765,7 @@ Section cmra_morphism.
End cmra_morphism. End cmra_morphism.
(** Functors *) (** Functors *)
Structure rFunctor := RFunctor { Record rFunctor := RFunctor {
rFunctor_car : ofeT ofeT cmraT; rFunctor_car : ofeT ofeT cmraT;
rFunctor_map {A1 A2 B1 B2} : rFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) rFunctor_car A1 B1 -n> rFunctor_car A2 B2; ((A2 -n> A1) * (B1 -n> B2)) rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
...@@ -798,7 +798,7 @@ Coercion constRF : cmraT >-> rFunctor. ...@@ -798,7 +798,7 @@ Coercion constRF : cmraT >-> rFunctor.
Instance constRF_contractive B : rFunctorContractive (constRF B). Instance constRF_contractive B : rFunctorContractive (constRF B).
Proof. rewrite /rFunctorContractive; apply _. Qed. Proof. rewrite /rFunctorContractive; apply _. Qed.
Structure urFunctor := URFunctor { Record urFunctor := URFunctor {
urFunctor_car : ofeT ofeT ucmraT; urFunctor_car : ofeT ofeT ucmraT;
urFunctor_map {A1 A2 B1 B2} : urFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) urFunctor_car A1 B1 -n> urFunctor_car A2 B2; ((A2 -n> A1) * (B1 -n> B2)) urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
......
...@@ -663,7 +663,7 @@ Instance prodC_map_ne {A A' B B'} : ...@@ -663,7 +663,7 @@ Instance prodC_map_ne {A A' B B'} :
Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed. Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
(** Functors *) (** Functors *)
Structure cFunctor := CFunctor { Record cFunctor := CFunctor {
cFunctor_car : ofeT ofeT ofeT; cFunctor_car : ofeT ofeT ofeT;
cFunctor_map {A1 A2 B1 B2} : cFunctor_map {A1 A2 B1 B2} :
((A2 -n> A1) * (B1 -n> B2)) cFunctor_car A1 B1 -n> cFunctor_car A2 B2; ((A2 -n> A1) * (B1 -n> B2)) cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
......
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