Commit ac1e918f by Robbert Krebbers

More prelude/base rearrangement.

parent dbb8d7c9
 ... @@ -316,7 +316,6 @@ Arguments compose _ _ _ _ _ _ /. ... @@ -316,7 +316,6 @@ Arguments compose _ _ _ _ _ _ /. Arguments flip _ _ _ _ _ _ /. Arguments flip _ _ _ _ _ _ /. Arguments const _ _ _ _ /. Arguments const _ _ _ _ /. Typeclasses Transparent id compose flip 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' := Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' := g ∘ h ∘ f. g ∘ h ∘ f. ... @@ -402,6 +401,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope. ... @@ -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 .1" := (fst p) (at level 10, format "p .1"). Notation "p .2" := (snd p) (at level 10, format "p .2"). Notation "p .2" := (snd p) (at level 10, format "p .2"). Instance: Params (@pair) 2. Notation curry := prod_curry. Notation curry := prod_curry. Notation uncurry := prod_uncurry. Notation uncurry := prod_uncurry. Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D := Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D := ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!