From c19c885de359dc391d36199844a8d0cdfb9cdc69 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 7 Jun 2017 11:34:09 -0400 Subject: [PATCH] fix [unfold] index --- algebra/free_group.hlean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean index 291a4a8..e8f53c0 100644 --- a/algebra/free_group.hlean +++ b/algebra/free_group.hlean @@ -60,10 +60,10 @@ namespace group end definition free_group_one [constructor] : FG X := class_of [] - definition free_group_inv [unfold 4] : FG X → FG X := + definition free_group_inv [unfold 3] : FG X → FG X := quotient_unary_map (reverse ∘ map sum.flip) (λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip)) - definition free_group_mul [unfold 4 5] : FG X → FG X → FG X := + definition free_group_mul [unfold 3 4] : FG X → FG X → FG X := quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s)))) section