[ base ] Change Reader to fix search for MonadReader instance (#2729)

This commit is contained in:
Aleksei Volkov 2022-10-22 21:13:52 +03:00 committed by GitHub
parent 542ebeae97
commit c906720ee3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 30 additions and 1 deletions

View File

@ -34,7 +34,7 @@ runReaderT s action = runReaderT' action s
||| This is `ReaderT` applied to `Identity`.
public export
Reader : (stateType : Type) -> (a : Type) -> Type
Reader s a = ReaderT s Identity a
Reader s = ReaderT s Identity
||| Unwrap and apply a Reader monad computation
public export %inline

View File

@ -0,0 +1,7 @@
module SearchReader
import Control.Monad.Identity
import Control.Monad.Reader
monadReaderInstance : MonadReader a (Reader a)
monadReaderInstance = %search

View File

@ -0,0 +1,6 @@
module SearchState
import Control.Monad.State
monadWriterInstance : MonadState a (State a)
monadWriterInstance = %search

View File

@ -0,0 +1,7 @@
module SearchWriter
import Control.Monad.Identity
import Control.Monad.Writer
monadWriterInstance : (Monoid a) => MonadWriter a (Writer a)
monadWriterInstance = %search

View File

@ -0,0 +1,3 @@
1/1: Building SearchReader (SearchReader.idr)
1/1: Building SearchWriter (SearchWriter.idr)
1/1: Building SearchState (SearchState.idr)

View File

@ -0,0 +1,6 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner -c SearchReader.idr
$1 --no-color --console-width 0 --no-banner -c SearchWriter.idr
$1 --no-color --console-width 0 --no-banner -c SearchState.idr