agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard

Revise definitions of `Data.List.Base.scanl|inits`; add `Data.List.NonEmpty.Base.scanl⁺|inits⁺`

Open jamesmckinna opened this issue 1 year ago • 5 comments

Fixes #2267 . See also the discussion on #2258 .

jamesmckinna avatar Jan 29 '24 12:01 jamesmckinna

Hmmm, looks as though I've screwed up the CHANGELOG.

jamesmckinna avatar Jan 29 '24 13:01 jamesmckinna

Yes, other than that, this looks really good!

JacquesCarette avatar Jan 29 '24 14:01 JacquesCarette

Hopefully that's sorted out now.

jamesmckinna avatar Jan 29 '24 17:01 jamesmckinna

So I think we've (now) agreed to find a better home for this (and #2258 ) under Data.List.Something. Suggestions welcome!

jamesmckinna avatar Jan 31 '24 00:01 jamesmckinna

Aaargh: Data.List.Kleene.*!

jamesmckinna avatar Jan 31 '24 00:01 jamesmckinna

Now see #2395

jamesmckinna avatar May 23 '24 13:05 jamesmckinna