feat(library/coercion): add simple trick for defining coercions to function-class in a convenient way, closes #31

library/hott/equiv.lean

@@ -45,17 +45,12 @@ Equiv_mk : Π
   (equiv_isequiv : IsEquiv equiv_fun),
 Equiv A B
 
-definition equiv_fun {A B : Type} (e : Equiv A B) : A → B :=
+definition equiv_fun [coercion] {A B : Type} (e : Equiv A B) : A → B :=
 Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e
 
--- TODO: use a type class instead?
-coercion equiv_fun : Equiv
-
 definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
 Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
 
--- coercion equiv_isequiv
-
 -- TODO: better symbol
 infix `<~>`:25 := Equiv
 notation e `⁻¹` := equiv_inv e

library/logic/classes/decidable.lean

@@ -99,7 +99,5 @@ end decidable
 inductive decidable_eq [class] (A : Type) : Type :=
 intro : (Π x y : A, decidable (x = y)) → decidable_eq A
 
-theorem of_decidable_eq [instance] {A : Type} (H : decidable_eq A) (x y : A) : decidable (x = y) :=
+theorem of_decidable_eq [instance] [coercion] {A : Type} (H : decidable_eq A) (x y : A) : decidable (x = y) :=
 decidable_eq.rec (λ H, H) H x y
-
-coercion of_decidable_eq : decidable_eq

src/library/coercion.cpp

@@ -344,12 +344,16 @@ environment add_coercion(environment const & env, name const & f, io_state const
     declaration d = env.get(f);
     expr t = d.get_type();
     check_pi(f, t);
-    while (is_pi(binding_body(t)))
+    optional<name> C;
+    while (is_pi(t)) {
+        expr d = get_app_fn(binding_domain(t));
+        if (is_constant(d))
+            C = const_name(d);
         t = binding_body(t);
-    expr C = get_app_fn(binding_domain(t));
-    if (!is_constant(C))
+    }
+    if (!C)
         throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion");
-    return add_coercion(env, f, const_name(C), ios);
+    return add_coercion(env, f, *C, ios);
 }
 
 optional<pair<name, unsigned>> is_coercion(environment const & env, name const & f) {