mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 09:49:24 +03:00
Remove Kleisli composition (not used anymore)
This commit is contained in:
parent
ef00018329
commit
0e7ba90e9f
@ -455,16 +455,6 @@ export %inline
|
||||
pure : a -> Core a
|
||||
pure x = MkCore (pure (pure x))
|
||||
|
||||
infixr 1 <=<
|
||||
|
||||
-- Right-to-left Kleisli composition of monads (specialised)
|
||||
export %inline
|
||||
(<=<) : (b -> Core c) -> (a -> Core b) -> (a -> Core c)
|
||||
(<=<) g f x
|
||||
= do y <- f x
|
||||
z <- g y
|
||||
pure z
|
||||
|
||||
export
|
||||
(<*>) : Core (a -> b) -> Core a -> Core b
|
||||
(<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |]
|
||||
|
@ -284,7 +284,6 @@ elabInstance env fc n fs
|
||||
Nothing => def
|
||||
(Just x) => pure x
|
||||
|
||||
|
||||
subsetOf : forall a. Eq a => List a -> List a -> Bool
|
||||
subsetOf subset set = length (intersect subset set) == length subset
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user