File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -47,7 +47,7 @@ infix 1 _⋆_
47
47
------------------------------------------------------------------------
48
48
-- Type definition
49
49
50
- -- The free moand can be defined as the least fixpoint `μ (C ⋆C X)`
50
+ -- The free monad can be defined as the least fixpoint `μ (C ⋆C X)`
51
51
52
52
_⋆C_ : ∀ {x s p} → Container s p → Set x → Container (s ⊔ x) p
53
53
C ⋆C X = const X ⊎ C
Original file line number Diff line number Diff line change @@ -272,7 +272,7 @@ drop m xs = proj₁ (proj₂ (splitAt m xs))
272
272
group : ∀ n k (xs : Vec A (n * k)) →
273
273
∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss
274
274
group zero k [] = ([] , refl)
275
- group (suc n) k xs =
275
+ group (suc n) k xs =
276
276
let ys , zs , eq-split = splitAt k xs in
277
277
let zss , eq-group = group n k zs in
278
278
(ys ∷ zss) , trans eq-split (cong (ys ++_) eq-group)
You can’t perform that action at this time.
0 commit comments