{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Data.Maybe.Categorical where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Category.Applicative.Indexed
import qualified MAlonzo.Code.Category.Functor
import qualified MAlonzo.Code.Category.Monad.Indexed
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Function.Identity.Categorical
d_functor_8 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Category.Functor.T_RawFunctor_24
d_functor_8 :: T_Level_18 -> T_RawFunctor_24
d_functor_8 ~T_Level_18
v0 = T_RawFunctor_24
du_functor_8
du_functor_8 :: MAlonzo.Code.Category.Functor.T_RawFunctor_24
du_functor_8 :: T_RawFunctor_24
du_functor_8
= ((T_Level_18 -> T_Level_18 -> (Any -> Any) -> Any -> Any)
-> T_RawFunctor_24)
-> Any -> T_RawFunctor_24
forall a b. a -> b
coe
(T_Level_18 -> T_Level_18 -> (Any -> Any) -> Any -> Any)
-> T_RawFunctor_24
MAlonzo.Code.Category.Functor.C_RawFunctor'46'constructor_241
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> ((Any -> Any) -> Maybe Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe (Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_68 Any
v2))
d_applicative_12 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38
d_applicative_12 :: T_Level_18 -> T_RawIApplicative_38
d_applicative_12 ~T_Level_18
v0 = T_RawIApplicative_38
du_applicative_12
du_applicative_12 ::
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38
du_applicative_12 :: T_RawIApplicative_38
du_applicative_12
= ((T_Level_18 -> Any -> Any -> Any)
-> (T_Level_18
-> T_Level_18 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_RawIApplicative_38)
-> Any -> Any -> T_RawIApplicative_38
forall a b. a -> b
coe
(T_Level_18 -> Any -> Any -> Any)
-> (T_Level_18
-> T_Level_18 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_RawIApplicative_38
MAlonzo.Code.Category.Applicative.Indexed.C_RawIApplicative'46'constructor_815
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (Any -> Maybe Any) -> Any
forall a b. a -> b
coe Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16))
((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 ->
((Any -> Any) -> Any -> Maybe Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Maybe Any -> Any
MAlonzo.Code.Data.Maybe.Base.du_maybe_36
(((Any -> Any) -> Maybe Any -> Maybe Any) -> Any
forall a b. a -> b
coe (Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_68)
(let v5 :: b
v5 = Maybe Any -> b
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 in
Any -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v6 -> Any
forall {b}. b
v5)))))
d_applicativeZero_16 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicativeZero_156
d_applicativeZero_16 :: T_Level_18 -> T_RawIApplicativeZero_156
d_applicativeZero_16 ~T_Level_18
v0 = T_RawIApplicativeZero_156
du_applicativeZero_16
du_applicativeZero_16 ::
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicativeZero_156
du_applicativeZero_16 :: T_RawIApplicativeZero_156
du_applicativeZero_16
= (T_RawIApplicative_38
-> (T_Level_18 -> Any -> Any -> Any) -> T_RawIApplicativeZero_156)
-> Any -> Any -> T_RawIApplicativeZero_156
forall a b. a -> b
coe
T_RawIApplicative_38
-> (T_Level_18 -> Any -> Any -> Any) -> T_RawIApplicativeZero_156
MAlonzo.Code.Category.Applicative.Indexed.C_RawIApplicativeZero'46'constructor_10911
(T_RawIApplicative_38 -> Any
forall a b. a -> b
coe T_RawIApplicative_38
du_applicative_12)
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v0 Any
v1 Any
v2 -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
d_alternative_20 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Category.Applicative.Indexed.T_RawIAlternative_210
d_alternative_20 :: T_Level_18 -> T_RawIAlternative_210
d_alternative_20 ~T_Level_18
v0 = T_RawIAlternative_210
du_alternative_20
du_alternative_20 ::
MAlonzo.Code.Category.Applicative.Indexed.T_RawIAlternative_210
du_alternative_20 :: T_RawIAlternative_210
du_alternative_20
= (T_RawIApplicativeZero_156
-> (T_Level_18 -> Any -> Any -> Any -> Any -> Any)
-> T_RawIAlternative_210)
-> Any -> Any -> T_RawIAlternative_210
forall a b. a -> b
coe
T_RawIApplicativeZero_156
-> (T_Level_18 -> Any -> Any -> Any -> Any -> Any)
-> T_RawIAlternative_210
MAlonzo.Code.Category.Applicative.Indexed.C_RawIAlternative'46'constructor_12491
(T_RawIApplicativeZero_156 -> Any
forall a b. a -> b
coe T_RawIApplicativeZero_156
du_applicativeZero_16)
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v0 Any
v1 Any
v2 ->
(Maybe Any -> Maybe Any -> Maybe Any) -> Any
forall a b. a -> b
coe Maybe Any -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du__'60''8739''62'__84))
d_monadT_26 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 -> () -> ()) ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32 ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32
d_monadT_26 :: T_Level_18
-> (T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18)
-> T_RawIMonad_32
-> T_RawIMonad_32
d_monadT_26 ~T_Level_18
v0 ~T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18
v1 T_RawIMonad_32
v2 = T_RawIMonad_32 -> T_RawIMonad_32
du_monadT_26 T_RawIMonad_32
v2
du_monadT_26 ::
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32 ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32
du_monadT_26 :: T_RawIMonad_32 -> T_RawIMonad_32
du_monadT_26 T_RawIMonad_32
v0
= ((T_Level_18 -> Any -> Any -> Any)
-> (T_Level_18
-> T_Level_18 -> Any -> Any -> Any -> Any -> (Any -> Any) -> Any)
-> T_RawIMonad_32)
-> Any -> Any -> T_RawIMonad_32
forall a b. a -> b
coe
(T_Level_18 -> Any -> Any -> Any)
-> (T_Level_18
-> T_Level_18 -> Any -> Any -> Any -> Any -> (Any -> Any) -> Any)
-> T_RawIMonad_32
MAlonzo.Code.Category.Monad.Indexed.C_RawIMonad'46'constructor_711
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 Any
v3 ->
(T_RawIMonad_32 -> T_Level_18 -> Any -> Any -> Any)
-> T_RawIMonad_32 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_RawIMonad_32 -> T_Level_18 -> Any -> Any -> Any
MAlonzo.Code.Category.Monad.Indexed.d_return_52 T_RawIMonad_32
v0 Any
forall {b}. b
erased
(T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (Any -> Any
forall a b. a -> b
coe Any
v3))))
((Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
(T_RawIMonad_32
-> T_Level_18
-> T_Level_18
-> Any
-> Any
-> Any
-> Any
-> (Any -> Any)
-> Any)
-> T_RawIMonad_32
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_RawIMonad_32
-> T_Level_18
-> T_Level_18
-> Any
-> Any
-> Any
-> Any
-> (Any -> Any)
-> Any
MAlonzo.Code.Category.Monad.Indexed.d__'62''62''61'__60 T_RawIMonad_32
v0 Any
forall {b}. b
erased
Any
forall {b}. b
erased (T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
(T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
(T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8) Any
v6
(((Any -> Any) -> Any -> Maybe Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Maybe Any -> Any
MAlonzo.Code.Data.Maybe.Base.du_maybe_36 (Any -> Any
forall a b. a -> b
coe Any
v7)
((T_RawIMonad_32 -> T_Level_18 -> Any -> Any -> Any)
-> T_RawIMonad_32 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_RawIMonad_32 -> T_Level_18 -> Any -> Any -> Any
MAlonzo.Code.Category.Monad.Indexed.d_return_52 T_RawIMonad_32
v0 Any
forall {b}. b
erased
(T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))))
d_monad_80 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32
d_monad_80 :: T_Level_18 -> T_RawIMonad_32
d_monad_80 ~T_Level_18
v0 = T_RawIMonad_32
du_monad_80
du_monad_80 :: MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32
du_monad_80 :: T_RawIMonad_32
du_monad_80
= (T_RawIMonad_32 -> T_RawIMonad_32) -> Any -> T_RawIMonad_32
forall a b. a -> b
coe
T_RawIMonad_32 -> T_RawIMonad_32
du_monadT_26
(T_RawIMonad_32 -> Any
forall a b. a -> b
coe T_RawIMonad_32
MAlonzo.Code.Function.Identity.Categorical.du_monad_16)
d_monadZero_84 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonadZero_174
d_monadZero_84 :: T_Level_18 -> T_RawIMonadZero_174
d_monadZero_84 ~T_Level_18
v0 = T_RawIMonadZero_174
du_monadZero_84
du_monadZero_84 ::
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonadZero_174
du_monadZero_84 :: T_RawIMonadZero_174
du_monadZero_84
= (T_RawIMonad_32
-> T_RawIApplicativeZero_156 -> T_RawIMonadZero_174)
-> Any -> Any -> T_RawIMonadZero_174
forall a b. a -> b
coe
T_RawIMonad_32 -> T_RawIApplicativeZero_156 -> T_RawIMonadZero_174
MAlonzo.Code.Category.Monad.Indexed.C_RawIMonadZero'46'constructor_10609
(T_RawIMonad_32 -> Any
forall a b. a -> b
coe T_RawIMonad_32
du_monad_80) (T_RawIApplicativeZero_156 -> Any
forall a b. a -> b
coe T_RawIApplicativeZero_156
du_applicativeZero_16)
d_monadPlus_88 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonadPlus_240
d_monadPlus_88 :: T_Level_18 -> T_RawIMonadPlus_240
d_monadPlus_88 ~T_Level_18
v0 = T_RawIMonadPlus_240
du_monadPlus_88
du_monadPlus_88 ::
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonadPlus_240
du_monadPlus_88 :: T_RawIMonadPlus_240
du_monadPlus_88
= (T_RawIMonad_32 -> T_RawIAlternative_210 -> T_RawIMonadPlus_240)
-> Any -> Any -> T_RawIMonadPlus_240
forall a b. a -> b
coe
T_RawIMonad_32 -> T_RawIAlternative_210 -> T_RawIMonadPlus_240
MAlonzo.Code.Category.Monad.Indexed.C_RawIMonadPlus'46'constructor_12775
(T_RawIMonad_32 -> Any
forall a b. a -> b
coe T_RawIMonad_32
du_monad_80) (T_RawIAlternative_210 -> Any
forall a b. a -> b
coe T_RawIAlternative_210
du_alternative_20)
d_sequenceA_126 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(() -> ()) ->
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38 ->
() -> Maybe AgdaAny -> AgdaAny
d_sequenceA_126 :: T_Level_18
-> (T_Level_18 -> T_Level_18)
-> T_RawIApplicative_38
-> T_Level_18
-> Maybe Any
-> Any
d_sequenceA_126 ~T_Level_18
v0 ~T_Level_18 -> T_Level_18
v1 T_RawIApplicative_38
v2 ~T_Level_18
v3 Maybe Any
v4 = T_RawIApplicative_38 -> Maybe Any -> Any
du_sequenceA_126 T_RawIApplicative_38
v2 Maybe Any
v4
du_sequenceA_126 ::
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38 ->
Maybe AgdaAny -> AgdaAny
du_sequenceA_126 :: T_RawIApplicative_38 -> Maybe Any -> Any
du_sequenceA_126 T_RawIApplicative_38
v0 Maybe Any
v1
= case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v2
-> let v3 :: b
v3 = T_Level_18 -> b
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
Any -> Any
forall a b. a -> b
coe
(let v4 :: b
v4 = T_Level_18 -> b
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
Any -> Any
forall a b. a -> b
coe
((T_RawFunctor_24
-> T_Level_18 -> T_Level_18 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_RawFunctor_24
-> T_Level_18 -> T_Level_18 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Category.Functor.d__'60''36''62'__30
((T_RawIApplicative_38 -> Any -> Any -> T_RawFunctor_24)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_RawIApplicative_38 -> Any -> Any -> T_RawFunctor_24
MAlonzo.Code.Category.Applicative.Indexed.du_rawFunctor_72 (T_RawIApplicative_38 -> Any
forall a b. a -> b
coe T_RawIApplicative_38
v0)
(Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v3) (Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v4))
Any
forall {b}. b
erased Any
forall {b}. b
erased ((Any -> Maybe Any) -> Any
forall a b. a -> b
coe Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16) Any
v2))
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> (T_RawIApplicative_38 -> T_Level_18 -> Any -> Any -> Any)
-> T_RawIApplicative_38 -> Any -> Any -> Maybe Any -> Any
forall a b. a -> b
coe
T_RawIApplicative_38 -> T_Level_18 -> Any -> Any -> Any
MAlonzo.Code.Category.Applicative.Indexed.d_pure_58 T_RawIApplicative_38
v0 Any
forall {b}. b
erased
(T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8) Maybe Any
v1
Maybe Any
_ -> Any
forall {b}. b
MAlonzo.RTE.mazUnreachableError
d_mapA_136 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(() -> ()) ->
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> AgdaAny
d_mapA_136 :: T_Level_18
-> (T_Level_18 -> T_Level_18)
-> T_RawIApplicative_38
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Maybe Any
-> Any
d_mapA_136 ~T_Level_18
v0 ~T_Level_18 -> T_Level_18
v1 T_RawIApplicative_38
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 Any -> Any
v6 Maybe Any
v7 = T_RawIApplicative_38 -> (Any -> Any) -> Maybe Any -> Any
du_mapA_136 T_RawIApplicative_38
v2 Any -> Any
v6 Maybe Any
v7
du_mapA_136 ::
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38 ->
(AgdaAny -> AgdaAny) -> Maybe AgdaAny -> AgdaAny
du_mapA_136 :: T_RawIApplicative_38 -> (Any -> Any) -> Maybe Any -> Any
du_mapA_136 T_RawIApplicative_38
v0 Any -> Any
v1 Maybe Any
v2
= (T_RawIApplicative_38 -> Maybe Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
T_RawIApplicative_38 -> Maybe Any -> Any
du_sequenceA_126 (T_RawIApplicative_38 -> Any
forall a b. a -> b
coe T_RawIApplicative_38
v0)
(((Any -> Any) -> Maybe Any -> Maybe Any)
-> (Any -> Any) -> Maybe Any -> Any
forall a b. a -> b
coe (Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_68 Any -> Any
v1 Maybe Any
v2)
d_forA_146 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(() -> ()) ->
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> () -> Maybe AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d_forA_146 :: T_Level_18
-> (T_Level_18 -> T_Level_18)
-> T_RawIApplicative_38
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Maybe Any
-> (Any -> Any)
-> Any
d_forA_146 ~T_Level_18
v0 ~T_Level_18 -> T_Level_18
v1 T_RawIApplicative_38
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 Maybe Any
v6 Any -> Any
v7 = T_RawIApplicative_38 -> Maybe Any -> (Any -> Any) -> Any
du_forA_146 T_RawIApplicative_38
v2 Maybe Any
v6 Any -> Any
v7
du_forA_146 ::
MAlonzo.Code.Category.Applicative.Indexed.T_RawIApplicative_38 ->
Maybe AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du_forA_146 :: T_RawIApplicative_38 -> Maybe Any -> (Any -> Any) -> Any
du_forA_146 T_RawIApplicative_38
v0 Maybe Any
v1 Any -> Any
v2 = (T_RawIApplicative_38 -> (Any -> Any) -> Maybe Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_RawIApplicative_38 -> (Any -> Any) -> Maybe Any -> Any
du_mapA_136 (T_RawIApplicative_38 -> Any
forall a b. a -> b
coe T_RawIApplicative_38
v0) ((Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any
v2) (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
v1)
d_forA_198 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(() -> ()) ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> () -> Maybe AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d_forA_198 :: T_Level_18
-> (T_Level_18 -> T_Level_18)
-> T_RawIMonad_32
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Maybe Any
-> (Any -> Any)
-> Any
d_forA_198 ~T_Level_18
v0 ~T_Level_18 -> T_Level_18
v1 T_RawIMonad_32
v2 = T_RawIMonad_32
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Maybe Any
-> (Any -> Any)
-> Any
du_forA_198 T_RawIMonad_32
v2
du_forA_198 ::
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> () -> Maybe AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du_forA_198 :: T_RawIMonad_32
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Maybe Any
-> (Any -> Any)
-> Any
du_forA_198 T_RawIMonad_32
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 Maybe Any
v4 Any -> Any
v5
= (T_RawIApplicative_38 -> Maybe Any -> (Any -> Any) -> Any)
-> Any -> Maybe Any -> (Any -> Any) -> Any
forall a b. a -> b
coe
T_RawIApplicative_38 -> Maybe Any -> (Any -> Any) -> Any
du_forA_146
((T_RawIMonad_32 -> T_RawIApplicative_38) -> Any -> Any
forall a b. a -> b
coe
T_RawIMonad_32 -> T_RawIApplicative_38
MAlonzo.Code.Category.Monad.Indexed.du_rawIApplicative_122
(T_RawIMonad_32 -> Any
forall a b. a -> b
coe T_RawIMonad_32
v0))
Maybe Any
v4 Any -> Any
v5
d_mapA_200 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(() -> ()) ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> AgdaAny
d_mapA_200 :: T_Level_18
-> (T_Level_18 -> T_Level_18)
-> T_RawIMonad_32
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Maybe Any
-> Any
d_mapA_200 ~T_Level_18
v0 ~T_Level_18 -> T_Level_18
v1 T_RawIMonad_32
v2 = T_RawIMonad_32
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Maybe Any
-> Any
du_mapA_200 T_RawIMonad_32
v2
du_mapA_200 ::
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> AgdaAny
du_mapA_200 :: T_RawIMonad_32
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> Maybe Any
-> Any
du_mapA_200 T_RawIMonad_32
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 Any -> Any
v4 Maybe Any
v5
= (T_RawIApplicative_38 -> (Any -> Any) -> Maybe Any -> Any)
-> Any -> (Any -> Any) -> Maybe Any -> Any
forall a b. a -> b
coe
T_RawIApplicative_38 -> (Any -> Any) -> Maybe Any -> Any
du_mapA_136
((T_RawIMonad_32 -> T_RawIApplicative_38) -> Any -> Any
forall a b. a -> b
coe
T_RawIMonad_32 -> T_RawIApplicative_38
MAlonzo.Code.Category.Monad.Indexed.du_rawIApplicative_122
(T_RawIMonad_32 -> Any
forall a b. a -> b
coe T_RawIMonad_32
v0))
Any -> Any
v4 Maybe Any
v5
d_sequenceA_202 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(() -> ()) ->
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32 ->
() -> Maybe AgdaAny -> AgdaAny
d_sequenceA_202 :: T_Level_18
-> (T_Level_18 -> T_Level_18)
-> T_RawIMonad_32
-> T_Level_18
-> Maybe Any
-> Any
d_sequenceA_202 ~T_Level_18
v0 ~T_Level_18 -> T_Level_18
v1 T_RawIMonad_32
v2 = T_RawIMonad_32 -> T_Level_18 -> Maybe Any -> Any
du_sequenceA_202 T_RawIMonad_32
v2
du_sequenceA_202 ::
MAlonzo.Code.Category.Monad.Indexed.T_RawIMonad_32 ->
() -> Maybe AgdaAny -> AgdaAny
du_sequenceA_202 :: T_RawIMonad_32 -> T_Level_18 -> Maybe Any -> Any
du_sequenceA_202 T_RawIMonad_32
v0 T_Level_18
v1 Maybe Any
v2
= (T_RawIApplicative_38 -> Maybe Any -> Any)
-> Any -> Maybe Any -> Any
forall a b. a -> b
coe
T_RawIApplicative_38 -> Maybe Any -> Any
du_sequenceA_126
((T_RawIMonad_32 -> T_RawIApplicative_38) -> Any -> Any
forall a b. a -> b
coe
T_RawIMonad_32 -> T_RawIApplicative_38
MAlonzo.Code.Category.Monad.Indexed.du_rawIApplicative_122
(T_RawIMonad_32 -> Any
forall a b. a -> b
coe T_RawIMonad_32
v0))
Maybe Any
v2