From e6ce5d9b722107fb1423b1f2f9b3a3c5682ad2fa Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 29 Jun 2015 21:24:38 +1000 Subject: [PATCH] refactor(library/data/fin): put fin.val coercion in fin namespace --- library/data/fin.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/data/fin.lean b/library/data/fin.lean index 34e3c4a7c..0cd4f91be 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -9,12 +9,13 @@ import data.list.basic data.finset.basic data.fintype.card algebra.group open eq.ops nat function list finset fintype structure fin (n : nat) := (val : nat) (is_lt : val < n) -attribute fin.val [coercion] definition less_than [reducible] := fin namespace fin +attribute fin.val [coercion] + section def_equal variable {n : nat}