From 178be8d8ea8c866db0ce1cf2b330245dca0f5d3f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Jan 2017 20:14:28 -0800 Subject: [PATCH] fix(library/init/coe): coe should be reducible --- library/init/coe.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/coe.lean b/library/init/coe.lean index 80016cecff..53c67b496b 100644 --- a/library/init/coe.lean +++ b/library/init/coe.lean @@ -64,13 +64,13 @@ has_coe_to_fun.coe /- User level coercion operators -/ -def coe {a : Type u} {b : Type v} [has_lift_t a b] : a → b := +@[reducible] def coe {a : Type u} {b : Type v} [has_lift_t a b] : a → b := lift_t -def coe_fn {a : Type u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x := +@[reducible] def coe_fn {a : Type u} [has_coe_to_fun.{u v} a] : Π x : a, has_coe_to_fun.F.{u v} x := has_coe_to_fun.coe -def coe_sort {a : Type u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a := +@[reducible] def coe_sort {a : Type u} [has_coe_to_sort.{u v} a] : a → has_coe_to_sort.S.{u v} a := has_coe_to_sort.coe /- Notation -/