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

fix(tests/lean/hott/443_b): adjust test to reflect changes in the HoTT library

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-28 08:46:00 -08:00
parent 1559e0e58c
commit dc62bc498f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/hott/443_b.hlean
View file

@ -1,6 +1,6 @@
import algebra.groupoid algebra.group import algebra.groupoid algebra.group
open eq sigma unit category morphism path_algebra equiv open eq sigma unit category path_algebra equiv
set_option pp.implicit true set_option pp.implicit true
set_option pp.universes true set_option pp.universes true