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

refactor(library/data/fin): put fin.val coercion in fin namespace

Browse source
This commit is contained in:
Jeremy Avigad 2015-06-29 21:24:38 +10:00
parent a54fb42f87
commit e6ce5d9b72
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/data/fin.lean
View file

@ -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}