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

fix(hott/algebra) fix previous commit by importing 'arity'

Browse source
This commit is contained in:
Jakob von Raumer 2015-03-19 10:48:15 -04:00 committed by Leonardo de Moura
parent 36a102bad2
commit 74824078a8
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/algebra/precategory/basic.hlean
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.precategory.basic
Authors: Floris van Doorn
-/
import types.trunc types.pi
import types.trunc types.pi arity
open eq is_trunc pi