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

fix(hott/init/hedberg): remove unnecessary import

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-19 19:01:07 -08:00
parent 2521dbb39e
commit f93278eab8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/init/hedberg.hlean
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
Hedberg's Theorem: every type with decidable equality is a hset
-/
prelude
import init.nat init.trunc
import init.trunc
open eq eq.ops nat truncation sigma
-- TODO(Leo): move const coll and path_coll to a different file?