diff --git a/prelude/base.v b/prelude/base.v index ff635a1a3cf0bc5b84a3fc2ba9aff9572e0f34cd..22752705fcfc727038368eb0053fb2d86e83e8c3 100644 --- a/prelude/base.v +++ b/prelude/base.v @@ -316,7 +316,6 @@ Arguments compose _ _ _ _ _ _ /. Arguments flip _ _ _ _ _ _ /. Arguments const _ _ _ _ /. Typeclasses Transparent id compose flip const. -Instance: Params (@pair) 2. Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' := g ∘ h ∘ f. @@ -402,6 +401,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"). +Instance: Params (@pair) 2. + Notation curry := prod_curry. Notation uncurry := prod_uncurry. Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=