idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-11 06:14:41 +03:00
Code Issues Projects Releases Wiki Activity
1,446 Commits 5 Branches 9 Tags 109 MiB
d36a234041
Commit Graph

445 Commits

Author SHA1 Message Date
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
efae2682bd
Merge pull request #896 from Russoul/toString-iterators 
Add withIteratorString
 2021-01-16 15:47:45 +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
Alex Gryzlov
c67fc5d7c0
add Inspect idiom (#919) 2021-01-16 14:18:34 +00:00
Edwin Brady
96257f23c3
Merge pull request #914 from stefan-hoeck/lazy-list-impls 
Eq, Ord, and Show instances for LazyList
 2021-01-16 14:07:26 +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
André Videla
bea840418a
Merge pull request #823 from andylokandy/path 
Changes to System.Path

- Rename `startWith` to `isBaseOf`
- Rename `stripPrefix` to `dropBase`
- Add `dropExtension`
- Add `splitPath`
 2021-01-14 22:09:04 +00:00
Andy Lok
4f8bd22b35 Use present tense in doc for Path 2021-01-14 05:26:42 +08:00
Andy Lok
f1d6d4d6f4 Use dot syntax to avoid path argument 2021-01-14 05:05:59 +08: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
stefan-hoeck
2301826a4e improved documentation for 'on' 2021-01-13 05:06:01 +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
530e62a156 Eq, Ord, and Show instances for LazyList 2021-01-11 11:45:56 +01: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
e99a9b0c84
Merge pull request #901 from andrevidela/fold-count 
Add count and foldMap to prelude
 2021-01-06 19:29:50 +00:00
André Videla
28c4d1e3bb Add count and foldMap to prelude 2021-01-05 21:59:01 +00:00