{-# 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.Relation.Unary.Any 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable
d_Any_18 :: p -> p -> p -> p -> p -> ()
d_Any_18 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
newtype T_Any_18 = C_just_30 AgdaAny
d_drop'45'just_46 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> ()) -> AgdaAny -> T_Any_18 -> AgdaAny
d_drop'45'just_46 :: () -> () -> () -> (AgdaAny -> ()) -> AgdaAny -> T_Any_18 -> AgdaAny
d_drop'45'just_46 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~AgdaAny
v4 T_Any_18
v5 = T_Any_18 -> AgdaAny
du_drop'45'just_46 T_Any_18
v5
du_drop'45'just_46 :: T_Any_18 -> AgdaAny
du_drop'45'just_46 :: T_Any_18 -> AgdaAny
du_drop'45'just_46 T_Any_18
v0
= case T_Any_18 -> T_Any_18
forall a b. a -> b
coe T_Any_18
v0 of
C_just_30 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
T_Any_18
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_just'45'equivalence_52 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_just'45'equivalence_52 :: () -> () -> () -> (AgdaAny -> ()) -> AgdaAny -> T_Equivalence_16
d_just'45'equivalence_52 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~AgdaAny
v4
= T_Equivalence_16
du_just'45'equivalence_52
du_just'45'equivalence_52 ::
MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_just'45'equivalence_52 :: T_Equivalence_16
du_just'45'equivalence_52
= ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_equivalence_56 ((AgdaAny -> T_Any_18) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30)
((T_Any_18 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Any_18 -> AgdaAny
du_drop'45'just_46)
d_map_58 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
Maybe AgdaAny -> T_Any_18 -> T_Any_18
d_map_58 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_Any_18
-> T_Any_18
d_map_58 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 T_Any_18
v8 = (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny -> T_Any_18 -> T_Any_18
du_map_58 AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 T_Any_18
v8
du_map_58 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
Maybe AgdaAny -> T_Any_18 -> T_Any_18
du_map_58 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny -> T_Any_18 -> T_Any_18
du_map_58 AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 T_Any_18
v2
= case T_Any_18 -> T_Any_18
forall a b. a -> b
coe T_Any_18
v2 of
C_just_30 AgdaAny
v4
-> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v5
-> (AgdaAny -> T_Any_18) -> AgdaAny -> T_Any_18
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v4)
Maybe AgdaAny
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Any_18
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
d_satisfied_66 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_satisfied_66 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> Maybe AgdaAny
-> T_Any_18
-> T_Σ_14
d_satisfied_66 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 Maybe AgdaAny
v4 T_Any_18
v5 = Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_satisfied_66 Maybe AgdaAny
v4 T_Any_18
v5
du_satisfied_66 ::
Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_satisfied_66 :: Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_satisfied_66 Maybe AgdaAny
v0 T_Any_18
v1
= case T_Any_18 -> T_Any_18
forall a b. a -> b
coe T_Any_18
v1 of
C_just_30 AgdaAny
v3
-> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v0 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.du_'45''44'__112 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
Maybe AgdaAny
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Any_18
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_zipWith_90 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Any_18
d_zipWith_90 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> (AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny
-> T_Σ_14
-> T_Any_18
d_zipWith_90 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> ()
v5 ~AgdaAny -> ()
v6 ~AgdaAny -> ()
v7 AgdaAny -> T_Σ_14 -> AgdaAny
v8 Maybe AgdaAny
v9 T_Σ_14
v10
= (AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zipWith_90 AgdaAny -> T_Σ_14 -> AgdaAny
v8 Maybe AgdaAny
v9 T_Σ_14
v10
du_zipWith_90 ::
(AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Any_18
du_zipWith_90 :: (AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zipWith_90 AgdaAny -> T_Σ_14 -> AgdaAny
v0 Maybe AgdaAny
v1 T_Σ_14
v2
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
-> case AgdaAny -> T_Any_18
forall a b. a -> b
coe AgdaAny
v3 of
C_just_30 AgdaAny
v6
-> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v7
-> case AgdaAny -> T_Any_18
forall a b. a -> b
coe AgdaAny
v4 of
C_just_30 AgdaAny
v9
-> (AgdaAny -> T_Any_18) -> AgdaAny -> T_Any_18
forall a b. a -> b
coe
AgdaAny -> T_Any_18
C_just_30
((AgdaAny -> T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Σ_14 -> AgdaAny
v0 AgdaAny
v7
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)))
T_Any_18
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
Maybe AgdaAny
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Any_18
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
d_unzipWith_98 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_unzipWith_98 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny
-> T_Any_18
-> T_Σ_14
d_unzipWith_98 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> ()
v5 ~AgdaAny -> ()
v6 ~AgdaAny -> ()
v7 AgdaAny -> AgdaAny -> T_Σ_14
v8 Maybe AgdaAny
v9 T_Any_18
v10
= (AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzipWith_98 AgdaAny -> AgdaAny -> T_Σ_14
v8 Maybe AgdaAny
v9 T_Any_18
v10
du_unzipWith_98 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_unzipWith_98 :: (AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzipWith_98 AgdaAny -> AgdaAny -> T_Σ_14
v0 Maybe AgdaAny
v1 T_Any_18
v2
= case T_Any_18 -> T_Any_18
forall a b. a -> b
coe T_Any_18
v2 of
C_just_30 AgdaAny
v4
-> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v5
-> ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148 ((AgdaAny -> T_Any_18) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30)
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> (AgdaAny -> T_Any_18) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30)) ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
v0 AgdaAny
v5 AgdaAny
v4)
Maybe AgdaAny
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Any_18
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_zip_120 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Any_18
d_zip_120 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> Maybe AgdaAny
-> T_Σ_14
-> T_Any_18
d_zip_120 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4 ~AgdaAny -> ()
v5 Maybe AgdaAny
v6 = Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zip_120 Maybe AgdaAny
v6
du_zip_120 ::
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Any_18
du_zip_120 :: Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zip_120 Maybe AgdaAny
v0 = ((AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny -> T_Σ_14 -> T_Any_18)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Any_18
forall a b. a -> b
coe (AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zipWith_90 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v0)
d_unzip_122 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_unzip_122 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> Maybe AgdaAny
-> T_Any_18
-> T_Σ_14
d_unzip_122 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4 ~AgdaAny -> ()
v5 Maybe AgdaAny
v6 = Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzip_122 Maybe AgdaAny
v6
du_unzip_122 ::
Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_unzip_122 :: Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzip_122 Maybe AgdaAny
v0
= ((AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny -> T_Any_18 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Any_18 -> T_Σ_14
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzipWith_98 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v0)
d_dec_136 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dec_136 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> T_Dec_32)
-> Maybe AgdaAny
-> T_Dec_32
d_dec_136 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5 = (AgdaAny -> T_Dec_32) -> Maybe AgdaAny -> T_Dec_32
du_dec_136 AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5
du_dec_136 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dec_136 :: (AgdaAny -> T_Dec_32) -> Maybe AgdaAny -> T_Dec_32
du_dec_136 AgdaAny -> T_Dec_32
v0 Maybe AgdaAny
v1
= case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v2
-> (T_Equivalence_16 -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
T_Equivalence_16 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.du_map_14
(T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
du_just'45'equivalence_52) ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v2)
Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_irrelevant_144 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
Maybe AgdaAny ->
T_Any_18 ->
T_Any_18 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_irrelevant_144 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T_Any_18
-> T_Any_18
-> T__'8801'__12
d_irrelevant_144 = ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T_Any_18
-> T_Any_18
-> T__'8801'__12
forall a. a
erased
d_satisfiable_152 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_satisfiable_152 :: () -> () -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14
d_satisfiable_152 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 T_Σ_14
v4 = T_Σ_14 -> T_Σ_14
du_satisfiable_152 T_Σ_14
v4
du_satisfiable_152 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_satisfiable_152 :: T_Σ_14 -> T_Σ_14
du_satisfiable_152 T_Σ_14
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
((AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16)
(\ AgdaAny
v1 AgdaAny
v2 -> (AgdaAny -> T_Any_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30 AgdaAny
v2) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v0)