michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library): export [reducible] annotations from function namespace to top-level

Browse source 
see issue #433
This commit is contained in:
Leonardo de Moura 2015-02-16 18:52:41 -08:00
parent 7fc216183e
commit 421a30d75c
3 changed files with 18 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
hott/init/function.hlean
View file

@ -18,23 +18,23 @@ definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
definition id [reducible] (a : A) : A :=
a
definition on_fun (f : B → B → C) (g : A → B) : A → A → C :=
definition on_fun [reducible] (f : B → B → C) (g : A → B) : A → A → C :=
λx y, f (g x) (g y)
definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
definition combine [reducible] (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
λx y, op (f x y) (g x y)
definition const {A : Type} (B : Type) (a : A) : B → A :=
definition const [reducible] (B : Type) (a : A) : B → A :=
λx, a
definition dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type}
definition dcompose [reducible] {B : A → Type} {C : Π {x : A}, B x → Type}
(f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
λx, f (g x)
definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
definition flip [reducible] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
λy x, f x y
definition app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x :=
definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
f x
precedence `∘'`:60
@ -53,3 +53,6 @@ notation f `-[` op `]-` g := combine f op g
notation a `⟨` f `⟩` b := f a b
end function
-- copy reducible annotations to top-level
export [reduce-hints] function

15
library/algebra/function.lean
View file

@ -17,23 +17,23 @@ definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
definition id [reducible] (a : A) : A :=
a
definition on_fun (f : B → B → C) (g : A → B) : A → A → C :=
definition on_fun [reducible] (f : B → B → C) (g : A → B) : A → A → C :=
λx y, f (g x) (g y)
definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
definition combine [reducible] (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
λx y, op (f x y) (g x y)
definition const {A : Type} (B : Type) (a : A) : B → A :=
definition const [reducible] (B : Type) (a : A) : B → A :=
λx, a
definition dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type}
definition dcompose [reducible] {B : A → Type} {C : Π {x : A}, B x → Type}
(f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
λx, f (g x)
definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
definition flip [reducible] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
λy x, f x y
definition app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x :=
definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
f x
precedence `∘'`:60
@ -47,3 +47,6 @@ infixr $ := app
notation f `-[` op `]-` g := combine f op g
end function
-- copy reducible annotations to top-level
export [reduce-hints] function

1
tests/lean/hott/433.hlean
View file

@ -94,7 +94,6 @@ namespace pi
definition transport_V [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
p⁻¹ ▹ u
open function
protected definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
/- Equivalences -/
definition isequiv_functor_pi [instance] (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')