{-# 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.Base 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.These.Base
import qualified MAlonzo.Code.Level
d_boolToMaybe_18 ::
Bool -> Maybe MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_boolToMaybe_18 :: Bool -> Maybe T_'8868'_6
d_boolToMaybe_18 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then (Any -> Maybe Any) -> Any -> Maybe T_'8868'_6
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(T_'8868'_6 -> Any
forall a b. a -> b
coe T_'8868'_6
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
else Maybe Any -> Maybe T_'8868'_6
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
d_is'45'just_20 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Maybe AgdaAny -> Bool
d_is'45'just_20 :: T_'8868'_6 -> T_'8868'_6 -> Maybe Any -> Bool
d_is'45'just_20 ~T_'8868'_6
v0 ~T_'8868'_6
v1 Maybe Any
v2 = Maybe Any -> Bool
du_is'45'just_20 Maybe Any
v2
du_is'45'just_20 :: Maybe AgdaAny -> Bool
du_is'45'just_20 :: Maybe Any -> Bool
du_is'45'just_20 Maybe Any
v0
= case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v0 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v1
-> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
Maybe Any
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
d_is'45'nothing_22 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Maybe AgdaAny -> Bool
d_is'45'nothing_22 :: T_'8868'_6 -> T_'8868'_6 -> Maybe Any -> Bool
d_is'45'nothing_22 ~T_'8868'_6
v0 ~T_'8868'_6
v1 Maybe Any
v2 = Maybe Any -> Bool
du_is'45'nothing_22 Maybe Any
v2
du_is'45'nothing_22 :: Maybe AgdaAny -> Bool
du_is'45'nothing_22 :: Maybe Any -> Bool
du_is'45'nothing_22 Maybe Any
v0
= (Bool -> Bool) -> Any -> Bool
forall a b. a -> b
coe
Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
((Maybe Any -> Bool) -> Any -> Any
forall a b. a -> b
coe Maybe Any -> Bool
du_is'45'just_20 (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
v0))
d_maybe_32 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(Maybe AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny
d_maybe_32 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> (Maybe Any -> T_'8868'_6)
-> (Any -> Any)
-> Any
-> Maybe Any
-> Any
d_maybe_32 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~Maybe Any -> T_'8868'_6
v3 Any -> Any
v4 Any
v5 Maybe Any
v6 = (Any -> Any) -> Any -> Maybe Any -> Any
du_maybe_32 Any -> Any
v4 Any
v5 Maybe Any
v6
du_maybe_32 ::
(AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny
du_maybe_32 :: (Any -> Any) -> Any -> Maybe Any -> Any
du_maybe_32 Any -> Any
v0 Any
v1 Maybe Any
v2
= case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v2 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v3 -> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v0 Any
v3
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Any -> Any
forall a b. a -> b
coe Any
v1
Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_maybe'8242'_44 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny
d_maybe'8242'_44 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> (Any -> Any)
-> Any
-> Maybe Any
-> Any
d_maybe'8242'_44 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 = (Any -> Any) -> Any -> Maybe Any -> Any
du_maybe'8242'_44
du_maybe'8242'_44 ::
(AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny
du_maybe'8242'_44 :: (Any -> Any) -> Any -> Maybe Any -> Any
du_maybe'8242'_44 = ((Any -> Any) -> Any -> Maybe Any -> Any)
-> (Any -> Any) -> Any -> Maybe Any -> Any
forall a b. a -> b
coe (Any -> Any) -> Any -> Maybe Any -> Any
du_maybe_32
d_fromMaybe_46 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> AgdaAny -> Maybe AgdaAny -> AgdaAny
d_fromMaybe_46 :: T_'8868'_6 -> T_'8868'_6 -> Any -> Maybe Any -> Any
d_fromMaybe_46 ~T_'8868'_6
v0 ~T_'8868'_6
v1 = Any -> Maybe Any -> Any
du_fromMaybe_46
du_fromMaybe_46 :: AgdaAny -> Maybe AgdaAny -> AgdaAny
du_fromMaybe_46 :: Any -> Maybe Any -> Any
du_fromMaybe_46 = ((Any -> Any) -> Any -> Maybe Any -> Any)
-> (Any -> Any) -> Any -> Maybe Any -> Any
forall a b. a -> b
coe (Any -> Any) -> Any -> Maybe Any -> Any
du_maybe'8242'_44 (\ Any
v0 -> Any
v0)
d_From'45'just_56 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> Maybe AgdaAny -> ()
d_From'45'just_56 :: T_'8868'_6 -> T_'8868'_6 -> Maybe Any -> T_'8868'_6
d_From'45'just_56 = T_'8868'_6 -> T_'8868'_6 -> Maybe Any -> T_'8868'_6
forall a. a
erased
d_from'45'just_60 :: Maybe AgdaAny -> AgdaAny
d_from'45'just_60 :: Maybe Any -> Any
d_from'45'just_60 Maybe Any
v0
= case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v0 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> (Any -> T_Lift_8) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
(T_'8868'_6 -> Any
forall a b. a -> b
coe T_'8868'_6
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_map_64 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d_map_64 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> (Any -> Any)
-> Maybe Any
-> Maybe Any
d_map_64 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 Any -> Any
v4 = (Any -> Any) -> Maybe Any -> Maybe Any
du_map_64 Any -> Any
v4
du_map_64 :: (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du_map_64 :: (Any -> Any) -> Maybe Any -> Maybe Any
du_map_64 Any -> Any
v0
= ((Any -> Any) -> Any -> Maybe Any -> Any)
-> Any -> Any -> Maybe Any -> Maybe Any
forall a b. a -> b
coe
(Any -> Any) -> Any -> Maybe Any -> Any
du_maybe_32
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 ->
(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) -> Any -> Any
forall a b. a -> b
coe Any -> Any
v0 Any
v1)))
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
d_ap_68 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Maybe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d_ap_68 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> Maybe (Any -> Any)
-> Maybe Any
-> Maybe Any
d_ap_68 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 Maybe (Any -> Any)
v4 = Maybe (Any -> Any) -> Maybe Any -> Maybe Any
du_ap_68 Maybe (Any -> Any)
v4
du_ap_68 ::
Maybe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du_ap_68 :: Maybe (Any -> Any) -> Maybe Any -> Maybe Any
du_ap_68 Maybe (Any -> Any)
v0
= case Maybe (Any -> Any) -> Maybe Any
forall a b. a -> b
coe Maybe (Any -> Any)
v0 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v1
-> ((Any -> Any) -> Maybe Any -> Maybe Any)
-> Any -> Maybe Any -> Maybe Any
forall a b. a -> b
coe (Any -> Any) -> Maybe Any -> Maybe Any
du_map_64 (Any -> Any
forall a b. a -> b
coe Any
v1)
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> (Any -> Maybe (Any -> Any)) -> Maybe Any -> Maybe Any
forall a b. a -> b
coe (\ Any
v1 -> Maybe (Any -> Any)
v0)
Maybe Any
_ -> Maybe Any -> Maybe Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'62''62''61'__72 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
d__'62''62''61'__72 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> Maybe Any
-> (Any -> Maybe Any)
-> Maybe Any
d__'62''62''61'__72 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 Maybe Any
v4 Any -> Maybe Any
v5
= Maybe Any -> (Any -> Maybe Any) -> Maybe Any
du__'62''62''61'__72 Maybe Any
v4 Any -> Maybe Any
v5
du__'62''62''61'__72 ::
Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
du__'62''62''61'__72 :: Maybe Any -> (Any -> Maybe Any) -> Maybe Any
du__'62''62''61'__72 Maybe Any
v0 Any -> Maybe Any
v1
= case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v0 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v2 -> (Any -> Maybe Any) -> Any -> Maybe Any
forall a b. a -> b
coe Any -> Maybe Any
v1 Any
v2
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v0
Maybe Any
_ -> Maybe Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'60''8739''62'__80 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''8739''62'__80 :: T_'8868'_6 -> T_'8868'_6 -> Maybe Any -> Maybe Any -> Maybe Any
d__'60''8739''62'__80 ~T_'8868'_6
v0 ~T_'8868'_6
v1 Maybe Any
v2 Maybe Any
v3 = Maybe Any -> Maybe Any -> Maybe Any
du__'60''8739''62'__80 Maybe Any
v2 Maybe Any
v3
du__'60''8739''62'__80 ::
Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
du__'60''8739''62'__80 :: Maybe Any -> Maybe Any -> Maybe Any
du__'60''8739''62'__80 Maybe Any
v0 Maybe Any
v1
= case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v0 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v2 -> Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v0
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v1
Maybe Any
_ -> Maybe Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_when_88 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Bool -> AgdaAny -> Maybe AgdaAny
d_when_88 :: T_'8868'_6 -> T_'8868'_6 -> Bool -> Any -> Maybe Any
d_when_88 ~T_'8868'_6
v0 ~T_'8868'_6
v1 Bool
v2 Any
v3 = Bool -> Any -> Maybe Any
du_when_88 Bool
v2 Any
v3
du_when_88 :: Bool -> AgdaAny -> Maybe AgdaAny
du_when_88 :: Bool -> Any -> Maybe Any
du_when_88 Bool
v0 Any
v1
= ((Any -> Any) -> Maybe Any -> Maybe Any)
-> (Any -> Any) -> Maybe T_'8868'_6 -> Maybe Any
forall a b. a -> b
coe (Any -> Any) -> Maybe Any -> Maybe Any
du_map_64 (\ Any
v2 -> Any
v1) (Bool -> Maybe T_'8868'_6
d_boolToMaybe_18 (Bool -> Bool
forall a b. a -> b
coe Bool
v0))
d_alignWith_94 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d_alignWith_94 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> (T_These_38 -> Any)
-> Maybe Any
-> Maybe Any
-> Maybe Any
d_alignWith_94 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 ~T_'8868'_6
v4 ~T_'8868'_6
v5 T_These_38 -> Any
v6 Maybe Any
v7 Maybe Any
v8
= (T_These_38 -> Any) -> Maybe Any -> Maybe Any -> Maybe Any
du_alignWith_94 T_These_38 -> Any
v6 Maybe Any
v7 Maybe Any
v8
du_alignWith_94 ::
(MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
du_alignWith_94 :: (T_These_38 -> Any) -> Maybe Any -> Maybe Any -> Maybe Any
du_alignWith_94 T_These_38 -> Any
v0 Maybe Any
v1 Maybe Any
v2
= case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v3
-> case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v2 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v4
-> (Any -> Maybe Any) -> Any -> Maybe Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_These_38 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_These_38 -> Any
v0 ((Any -> Any -> T_These_38) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_These_38
MAlonzo.Code.Data.These.Base.C_these_52 (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v4)))
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> (Any -> Maybe Any) -> Any -> Maybe Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_These_38 -> Any) -> Any -> Any
forall a b. a -> b
coe T_These_38 -> Any
v0 ((Any -> T_These_38) -> Any -> Any
forall a b. a -> b
coe Any -> T_These_38
MAlonzo.Code.Data.These.Base.C_this_48 (Any -> Any
forall a b. a -> b
coe Any
v3)))
Maybe Any
_ -> Maybe Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v2 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v3
-> (Any -> Maybe Any) -> Any -> Maybe Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_These_38 -> Any) -> Any -> Any
forall a b. a -> b
coe T_These_38 -> Any
v0 ((Any -> T_These_38) -> Any -> Any
forall a b. a -> b
coe Any -> T_These_38
MAlonzo.Code.Data.These.Base.C_that_50 (Any -> Any
forall a b. a -> b
coe Any
v3)))
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v2
Maybe Any
_ -> Maybe Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Maybe Any
_ -> Maybe Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_zipWith_112 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d_zipWith_112 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> (Any -> Any -> Any)
-> Maybe Any
-> Maybe Any
-> Maybe Any
d_zipWith_112 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 ~T_'8868'_6
v4 ~T_'8868'_6
v5 Any -> Any -> Any
v6 Maybe Any
v7 Maybe Any
v8
= (Any -> Any -> Any) -> Maybe Any -> Maybe Any -> Maybe Any
du_zipWith_112 Any -> Any -> Any
v6 Maybe Any
v7 Maybe Any
v8
du_zipWith_112 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
du_zipWith_112 :: (Any -> Any -> Any) -> Maybe Any -> Maybe Any -> Maybe Any
du_zipWith_112 Any -> Any -> Any
v0 Maybe Any
v1 Maybe Any
v2
= let v3 :: b
v3 = 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 -> Maybe Any
forall a b. a -> b
coe
(case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v4
-> case Maybe Any -> Maybe Any
forall a b. a -> b
coe Maybe Any
v2 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v5
-> (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 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
v0 Any
v4 Any
v5)
Maybe Any
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3
Maybe Any
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3)
d_align_120 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny ->
Maybe AgdaAny -> Maybe MAlonzo.Code.Data.These.Base.T_These_38
d_align_120 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> Maybe Any
-> Maybe Any
-> Maybe T_These_38
d_align_120 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 = Maybe Any -> Maybe Any -> Maybe T_These_38
du_align_120
du_align_120 ::
Maybe AgdaAny ->
Maybe AgdaAny -> Maybe MAlonzo.Code.Data.These.Base.T_These_38
du_align_120 :: Maybe Any -> Maybe Any -> Maybe T_These_38
du_align_120 = ((T_These_38 -> Any) -> Maybe Any -> Maybe Any -> Maybe Any)
-> Any -> Maybe Any -> Maybe Any -> Maybe T_These_38
forall a b. a -> b
coe (T_These_38 -> Any) -> Maybe Any -> Maybe Any -> Maybe Any
du_alignWith_94 ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 -> Any
v0))
d_zip_122 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny ->
Maybe AgdaAny -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_zip_122 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> Maybe Any
-> Maybe Any
-> Maybe T_Σ_14
d_zip_122 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 = Maybe Any -> Maybe Any -> Maybe T_Σ_14
du_zip_122
du_zip_122 ::
Maybe AgdaAny ->
Maybe AgdaAny -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_zip_122 :: Maybe Any -> Maybe Any -> Maybe T_Σ_14
du_zip_122
= ((Any -> Any -> Any) -> Maybe Any -> Maybe Any -> Maybe Any)
-> Any -> Maybe Any -> Maybe Any -> Maybe T_Σ_14
forall a b. a -> b
coe
(Any -> Any -> Any) -> Maybe Any -> Maybe Any -> Maybe Any
du_zipWith_112 ((Any -> Any -> T_Σ_14) -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32)
d_thisM_124 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny -> Maybe AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38
d_thisM_124 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> Any
-> Maybe Any
-> T_These_38
d_thisM_124 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 Any
v4 = Any -> Maybe Any -> T_These_38
du_thisM_124 Any
v4
du_thisM_124 ::
AgdaAny -> Maybe AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38
du_thisM_124 :: Any -> Maybe Any -> T_These_38
du_thisM_124 Any
v0
= ((Any -> Any) -> Any -> Maybe Any -> Any)
-> Any -> Any -> Maybe Any -> T_These_38
forall a b. a -> b
coe
(Any -> Any) -> Any -> Maybe Any -> Any
du_maybe'8242'_44
((Any -> Any -> T_These_38) -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_These_38
MAlonzo.Code.Data.These.Base.C_these_52 (Any -> Any
forall a b. a -> b
coe Any
v0))
((Any -> T_These_38) -> Any -> Any
forall a b. a -> b
coe Any -> T_These_38
MAlonzo.Code.Data.These.Base.C_this_48 (Any -> Any
forall a b. a -> b
coe Any
v0))
d_thatM_128 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny -> AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38
d_thatM_128 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> Maybe Any
-> Any
-> T_These_38
d_thatM_128 ~T_'8868'_6
v0 ~T_'8868'_6
v1 ~T_'8868'_6
v2 ~T_'8868'_6
v3 = Maybe Any -> Any -> T_These_38
du_thatM_128
du_thatM_128 ::
Maybe AgdaAny -> AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38
du_thatM_128 :: Maybe Any -> Any -> T_These_38
du_thatM_128
= ((Any -> Any) -> Any -> Maybe Any -> Any)
-> Any -> Any -> Maybe Any -> Any -> T_These_38
forall a b. a -> b
coe
(Any -> Any) -> Any -> Maybe Any -> Any
du_maybe'8242'_44 ((Any -> Any -> T_These_38) -> Any
forall a b. a -> b
coe Any -> Any -> T_These_38
MAlonzo.Code.Data.These.Base.C_these_52)
((Any -> T_These_38) -> Any
forall a b. a -> b
coe Any -> T_These_38
MAlonzo.Code.Data.These.Base.C_that_50)