mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
Revert "[ fix ] Rename Prelude.Interface NS Lazy to ILazy"
This reverts commit bd231c2076
, which is a
separate thing that should be its own PR.
This commit is contained in:
parent
bcbe2b8c4f
commit
009eb270c1
@ -88,10 +88,6 @@
|
||||
|
||||
* Constant folding of trivial let statements and `believe_me`.
|
||||
|
||||
* Moved `Lazy`, `Inf`, `Delay`, and `Force` from magic strings to reserved
|
||||
compiler primitives. This may mean that certian namespaces and libararies need
|
||||
renaming (see, for example, the `Prelude.Interfaces` change below).
|
||||
|
||||
### Library changes
|
||||
|
||||
#### Prelude
|
||||
@ -106,9 +102,6 @@
|
||||
|
||||
* Added `Compose` instances for `Bifunctor`, `Bifoldable` and `Bitraversable`.
|
||||
|
||||
* Rename the `Lazy` namespace in `Interfaces` to `ILazy` due to `Lazy` now being
|
||||
a reserved compiler primitive.
|
||||
|
||||
#### Base
|
||||
|
||||
* Deprecates `setByte` and `getByte` from `Data.Buffer` for removal in a future
|
||||
|
@ -449,13 +449,13 @@ public export
|
||||
[MonoidApplicative] Applicative f => Monoid a => Monoid (f a) using SemigroupApplicative where
|
||||
neutral = pure neutral
|
||||
|
||||
namespace ILazy
|
||||
namespace Lazy
|
||||
public export
|
||||
[SemigroupAlternative] Alternative f => Semigroup (Lazy (f a)) where
|
||||
x <+> y = force x <|> y
|
||||
|
||||
public export
|
||||
[MonoidAlternative] Alternative f => Monoid (Lazy (f a)) using ILazy.SemigroupAlternative where
|
||||
[MonoidAlternative] Alternative f => Monoid (Lazy (f a)) using Lazy.SemigroupAlternative where
|
||||
neutral = delay empty
|
||||
|
||||
public export
|
||||
@ -488,7 +488,7 @@ public export
|
||||
||| Note: In Haskell, `choice` is called `asum`.
|
||||
%inline public export
|
||||
choice : Alternative f => Foldable t => t (Lazy (f a)) -> f a
|
||||
choice = force . concat @{ILazy.MonoidAlternative}
|
||||
choice = force . concat @{Lazy.MonoidAlternative}
|
||||
|
||||
||| A fused version of `choice` and `map`.
|
||||
%inline public export
|
||||
|
Loading…
Reference in New Issue
Block a user