max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/coe): make sure base case is tried before transitive case, add (decidable (coe b)) instance

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-30 11:44:05 -07:00
parent 4f72fa5fc5
commit 32eb37472f
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
library/init/coe.lean
View file

@ -71,18 +71,18 @@ notation `⇑`:max a:max := coe_fn a
/- Transitive closure for has_lift, has_coe, has_coe_to_fun -/
definition lift_base [instance] {A B : Type} [has_lift A B] : has_lift_t A B :=
has_lift_t.mk lift
definition lift_trans [instance] {A B C : Type} [has_lift A B] [has_lift_t B C] : has_lift_t A C :=
has_lift_t.mk (λ a, lift_t (lift a : B))
definition coe_base [instance] {A B : Type} [has_coe A B] : has_coe_t A B :=
has_coe_t.mk coe_b
definition lift_base [instance] {A B : Type} [has_lift A B] : has_lift_t A B :=
has_lift_t.mk lift
definition coe_trans [instance] {A B C : Type} [has_coe A B] [has_coe_t B C] : has_coe_t A C :=
has_coe_t.mk (λ a, coe_t (coe_b a : B))
definition coe_base [instance] {A B : Type} [has_coe A B] : has_coe_t A B :=
has_coe_t.mk coe_b
definition coe_fn_trans [instance] {A B : Type} [has_lift_t A B] [has_coe_to_fun B] : has_coe_to_fun A :=
has_coe_to_fun.mk (has_coe_to_fun.F B) (λ a, coe_fn (coe a))
@ -96,6 +96,9 @@ has_lift_t.mk coe_t
definition coe_bool_to_Prop [instance] : has_coe bool Prop :=
has_coe.mk (λ b, b = tt)
definition coe_decidable_eq [instance] (b : bool) : decidable (coe b) :=
show decidable (b = tt), from _
definition coe_subtype [instance] {A : Type} {P : A → Prop} : has_coe {a \ P a} A :=
has_coe.mk (λ s, subtype.elt_of s)