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

refactor(library/data/fin): remove unnecessary import

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-13 16:35:59 -08:00
parent 37e852ba61
commit e4b9a89f5f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/fin.lean
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
Finite ordinals.
-/
import data.nat logic.cast
import data.nat
open nat
inductive fin : nat → Type :=