From c1d1a5e509a8f3235aaaf3d7201323b83cf89dbf Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 9 Dec 2015 17:12:37 -0500 Subject: [PATCH] There have been some changes in the algebra-part of Lean. We now need to import algebra.bundled in group_theory.basic --- group_theory/basic.hlean | 5 ++--- group_theory/constructions.hlean | 1 + 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/group_theory/basic.hlean b/group_theory/basic.hlean index 1cca2da..1419ba1 100644 --- a/group_theory/basic.hlean +++ b/group_theory/basic.hlean @@ -10,13 +10,12 @@ Basic group theory /- Groups are defined in the HoTT library in algebra/group, as part of the algebraic hierarchy. However, there is currently no group theory. - The only relevant defintions are the trivial group (in types/unit) and some files in algebra/ -/ -import algebra.group types.pointed types.pi +import types.pointed types.pi algebra.bundled open eq algebra pointed function is_trunc pi - +set_option class.force_new true namespace group definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one diff --git a/group_theory/constructions.hlean b/group_theory/constructions.hlean index 6f6b558..39dd861 100644 --- a/group_theory/constructions.hlean +++ b/group_theory/constructions.hlean @@ -10,6 +10,7 @@ import .basic hit.set_quotient types.sigma types.list types.sum open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function equiv +set_option class.force_new true namespace group /- Subgroups -/