stefan-hoeck
92b9833ee2
fixed doc for WriterT
2021-01-21 13:25:48 +01:00
stefan-hoeck
fd4851c0f5
strict, not stricht
2021-01-21 13:24:40 +01:00
stefan-hoeck
d36a234041
finished MonadRWS
2021-01-20 05:58:19 +01:00
stefan-hoeck
e906b28cae
removed MonadState functions from RWS.CPS.idr
2021-01-20 05:51:39 +01:00
stefan-hoeck
e8f2f56768
removed MonadWriter functions from RWS.CPS.idr
2021-01-20 05:48:43 +01:00
stefan-hoeck
6f2e358f1b
removed MonadReader functions from RWS.CPS.idr
2021-01-20 05:45:32 +01:00
stefan-hoeck
2776eaa1b1
remove MonadWriter functions from Writer.CPS module
2021-01-20 05:41:01 +01:00
stefan-hoeck
b6e5ba0830
minor MonadWriter cleanup
2021-01-20 05:27:56 +01:00
stefan-hoeck
313f52a88a
explicit lambdas for mapXYZ functions
2021-01-20 05:27:08 +01:00
stefan-hoeck
a42a34e9f0
removed trailing whitespace
2021-01-19 17:53:42 +01:00
stefan-hoeck
b5ab96477c
some cleanups in State
2021-01-19 17:47:06 +01:00
stefan-hoeck
8c9e318a6d
some cleanups in Reader
2021-01-19 17:43:47 +01:00
stefan-hoeck
7999420e88
made functions in EitherT and MaybeT public export
2021-01-19 17:38:59 +01:00
stefan-hoeck
c75d14fa8a
implemented MonadWriter
2021-01-19 16:19:27 +01:00
stefan-hoeck
01ba3aa365
moved MonadState to its interface module
2021-01-19 15:45:19 +01:00
stefan-hoeck
dac566152b
moved MonadReader to its interface module
2021-01-19 15:12:36 +01:00
stefan-hoeck
12f1ff493e
added mapStateT function
2021-01-19 14:57:10 +01:00
stefan-hoeck
8eb0e855f1
removed RWST function reader
2021-01-19 14:41:26 +01:00
stefan-hoeck
8cb2220e58
implemented cps-style Writer
2021-01-19 14:34:15 +01:00
stefan-hoeck
b9f7683fbd
mapRWST needs only a Functor
2021-01-19 14:11:06 +01:00
stefan-hoeck
b2e7384a80
implemented cps-style RWST
2021-01-19 13:58:18 +01:00
stefan-hoeck
81efdd7992
implementations for MonadError
2021-01-19 12:35:05 +01:00
stefan-hoeck
124afd89b1
moved transformer impls to their own directory
2021-01-19 11:53:23 +01:00
stefan-hoeck
b926e13b96
new transformer layout
2021-01-19 11:45:54 +01:00
Stiopa Koltsov
7264d40c56
Make isElem, DecEq public, not just export
...
... so they could be used in proof search.
Follow-up to #942
2021-01-18 10:37:57 +00:00
Edwin Brady
c7783c553c
Make the linter happier
2021-01-16 17:18:38 +00:00
Edwin Brady
6df2955a72
Merge pull request #909 from stefan-hoeck/maybeT
...
added MaybeT monad transformer to base
2021-01-16 15:43:14 +00:00
Edwin Brady
70c87e49da
Merge pull request #920 from stefan-hoeck/eithert-foldable-fix
...
fixed bug in Foldable of EitherT
2021-01-16 15:40:33 +00:00
Stiopa Koltsov
b76c9d91e0
Remove trailing whitespaces and add trailing newlines
2021-01-16 10:00:03 +00:00
Denis Buzdalov
4f05d227a6
List-level quantifier conversion to element-level and vice-versa
2021-01-15 18:57:01 +00:00
Denis Buzdalov
bcc8da5a6d
Currying and uncurrying functions for dependent pairs were added.
2021-01-15 18:53:40 +00:00
Denis Buzdalov
6d2dd935c4
Special variants of DPair as records ( #922 )
2021-01-15 17:19:20 +00:00
stefan-hoeck
7b73072554
fixed bug in Foldable of EitherT
2021-01-13 13:21:20 +01:00
Stefan Hoeck
77a911aa8a
Update libs/base/Control/Monad/Maybe.idr
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-01-13 11:19:03 +01:00
stefan-hoeck
e52b658d78
no linearity annotation for MkMaybeT
2021-01-13 05:34:07 +01:00
Edwin Brady
3621c5d1bd
Merge pull request #879 from edwinb/no-linearity-subtyping
...
Remove linearity subtyping
2021-01-12 12:33:26 +00:00
Edwin Brady
d4abbfdae2
Add HasLinearIO
...
Ideally, liftIO would always be linear, but that has lots of knock-on
effects for other monads which we might want to put in HasIO, now that
subtyping is gone. We'll have to revisit this when we have some kind of
multiplicity polymorphism.
2021-01-11 11:24:43 +00:00
stefan-hoeck
c39df89f84
deleted 'head' from Data.Stream
2021-01-11 09:36:13 +00:00
stefan-hoeck
31f50a793c
added prelude function 'on'
2021-01-11 05:26:17 +01:00
stefan-hoeck
c1912cb212
Monad prerequisite for Semigroup instance
2021-01-11 05:05:33 +01:00
stefan-hoeck
e71c7b8946
added MaybeT monad transformer to base
2021-01-08 06:04:41 +01:00
André Videla
3478297557
Merge pull request #905 from alebahn/master
...
Add public export to types/functions in Data.Fin.Order
2021-01-07 13:46:23 +00:00
André Videla
e4fcd4a089
Merge pull request #900 from andrevidela/vect-snoc
...
Add `snoc` to Data.Vect
2021-01-05 21:54:47 +00:00
Michael Messer
a1f3424ab8
Remove lamdaRequire
2021-01-05 16:30:11 +00:00
Aaron Lebahn
ce6465e279
Add public export to types/functions in Data.Fin.Order
2021-01-05 07:56:04 -06:00
André Videla
738c9d77d2
Add snoc to Data.Vect
...
Snoc add an element at the end of the vector. The main use case
for such a function is to get the expected type signature
Vect n a -> a -> Vect (S n) a instead of
Vect n a -> a -> Vect (n + 1) a which you get by using `++ [x]`
Snoc gets is name from `cons` by reversin each letter, indicating
tacking on the element at the end rather than the begining.
`append` would also be a suitable name.
2021-01-03 21:48:31 +00:00
Edwin Brady
cc6530026d
Merge github.com:idris-lang/Idris2 into no-linearity-subtyping
2020-12-29 21:37:56 +00:00
Edwin Brady
8d034a0a91
Relax some linearities in the base libraries
2020-12-29 21:34:35 +00:00
Edwin Brady
b75dcd5c17
Some multiplicity fixes in the libraries
2020-12-29 21:25:00 +00:00
Joey Eremondi
0eef8e58f9
Some utilities for Fin, relations and decidability ( #857 )
2020-12-28 21:41:12 +00:00
