From 1fff624e99c05caf31ca937ff2ed1961a1c4e008 Mon Sep 17 00:00:00 2001 From: Martin Fredin Date: Sun, 24 Sep 2023 23:02:54 +0200 Subject: [PATCH] Fix typo and whitespace violation --- src/Data/Container/FreeMonad.agda | 2 +- src/Data/Vec/Base.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Container/FreeMonad.agda b/src/Data/Container/FreeMonad.agda index 8a24ef1d36..d848915983 100644 --- a/src/Data/Container/FreeMonad.agda +++ b/src/Data/Container/FreeMonad.agda @@ -47,7 +47,7 @@ infix 1 _⋆_ ------------------------------------------------------------------------ -- Type definition --- The free moand can be defined as the least fixpoint `μ (C ⋆C X)` +-- The free monad can be defined as the least fixpoint `μ (C ⋆C X)` _⋆C_ : ∀ {x s p} → Container s p → Set x → Container (s ⊔ x) p C ⋆C X = const X ⊎ C diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 6752ec1b06..ed8817c66e 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -272,7 +272,7 @@ drop m xs = proj₁ (proj₂ (splitAt m xs)) group : ∀ n k (xs : Vec A (n * k)) → ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss group zero k [] = ([] , refl) -group (suc n) k xs = +group (suc n) k xs = let ys , zs , eq-split = splitAt k xs in let zss , eq-group = group n k zs in (ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group)