{-# 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.List.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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Sum
d_Any_34 :: p -> p -> p -> p -> p -> ()
d_Any_34 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Any_34 = C_here_46 AgdaAny | C_there_54 T_Any_34
d_head_56 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
[AgdaAny] ->
AgdaAny ->
(T_Any_34 -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
T_Any_34 -> AgdaAny
d_head_56 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> [AgdaAny]
-> AgdaAny
-> (T_Any_34 -> T_'8869'_4)
-> T_Any_34
-> AgdaAny
d_head_56 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~[AgdaAny]
v4 ~AgdaAny
v5 ~T_Any_34 -> T_'8869'_4
v6 T_Any_34
v7 = T_Any_34 -> AgdaAny
du_head_56 T_Any_34
v7
du_head_56 :: T_Any_34 -> AgdaAny
du_head_56 :: T_Any_34 -> AgdaAny
du_head_56 T_Any_34
v0
= case T_Any_34 -> T_Any_34
forall a b. a -> b
coe T_Any_34
v0 of
C_here_46 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
C_there_54 T_Any_34
v3
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_24
T_Any_34
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_tail_66 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] ->
(AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
T_Any_34 -> T_Any_34
d_tail_66 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_'8869'_4)
-> T_Any_34
-> T_Any_34
d_tail_66 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~AgdaAny
v4 ~[AgdaAny]
v5 ~AgdaAny -> T_'8869'_4
v6 T_Any_34
v7 = T_Any_34 -> T_Any_34
du_tail_66 T_Any_34
v7
du_tail_66 :: T_Any_34 -> T_Any_34
du_tail_66 :: T_Any_34 -> T_Any_34
du_tail_66 T_Any_34
v0
= case T_Any_34 -> T_Any_34
forall a b. a -> b
coe T_Any_34
v0 of
C_here_46 AgdaAny
v3 -> AgdaAny -> T_Any_34
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.du_'8869''45'elim_10
C_there_54 T_Any_34
v3 -> T_Any_34 -> T_Any_34
forall a b. a -> b
coe T_Any_34
v3
T_Any_34
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_map_76 ::
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) ->
[AgdaAny] -> T_Any_34 -> T_Any_34
d_map_76 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> T_Any_34
-> T_Any_34
d_map_76 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 T_Any_34
v8 = (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
du_map_76 AgdaAny -> AgdaAny -> AgdaAny
v6 [AgdaAny]
v7 T_Any_34
v8
du_map_76 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
[AgdaAny] -> T_Any_34 -> T_Any_34
du_map_76 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
du_map_76 AgdaAny -> AgdaAny -> AgdaAny
v0 [AgdaAny]
v1 T_Any_34
v2
= case T_Any_34 -> T_Any_34
forall a b. a -> b
coe T_Any_34
v2 of
C_here_46 AgdaAny
v5
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
(:) AgdaAny
v6 [AgdaAny]
v7 -> (AgdaAny -> T_Any_34) -> AgdaAny -> T_Any_34
forall a b. a -> b
coe AgdaAny -> T_Any_34
C_here_46 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v6 AgdaAny
v5)
[AgdaAny]
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
C_there_54 T_Any_34
v5
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
(:) AgdaAny
v6 [AgdaAny]
v7
-> (T_Any_34 -> T_Any_34) -> AgdaAny -> T_Any_34
forall a b. a -> b
coe T_Any_34 -> T_Any_34
C_there_54 (((AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
du_map_76 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v7) (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v5))
[AgdaAny]
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Any_34
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_index_86 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
[AgdaAny] -> T_Any_34 -> MAlonzo.Code.Data.Fin.Base.T_Fin_6
d_index_86 :: ()
-> () -> () -> (AgdaAny -> ()) -> [AgdaAny] -> T_Any_34 -> T_Fin_6
d_index_86 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 [AgdaAny]
v4 T_Any_34
v5 = [AgdaAny] -> T_Any_34 -> T_Fin_6
du_index_86 [AgdaAny]
v4 T_Any_34
v5
du_index_86 ::
[AgdaAny] -> T_Any_34 -> MAlonzo.Code.Data.Fin.Base.T_Fin_6
du_index_86 :: [AgdaAny] -> T_Any_34 -> T_Fin_6
du_index_86 [AgdaAny]
v0 T_Any_34
v1
= case T_Any_34 -> T_Any_34
forall a b. a -> b
coe T_Any_34
v1 of
C_here_46 AgdaAny
v4 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
C_there_54 T_Any_34
v4
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
(:) AgdaAny
v5 [AgdaAny]
v6
-> (T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(([AgdaAny] -> T_Any_34 -> T_Fin_6) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Fin_6
du_index_86 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v4))
[AgdaAny]
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Any_34
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
d_lookup_94 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
[AgdaAny] -> (AgdaAny -> ()) -> T_Any_34 -> AgdaAny
d_lookup_94 :: ()
-> () -> () -> [AgdaAny] -> (AgdaAny -> ()) -> T_Any_34 -> AgdaAny
d_lookup_94 ~()
v0 ~()
v1 ~()
v2 [AgdaAny]
v3 ~AgdaAny -> ()
v4 T_Any_34
v5 = [AgdaAny] -> T_Any_34 -> AgdaAny
du_lookup_94 [AgdaAny]
v3 T_Any_34
v5
du_lookup_94 :: [AgdaAny] -> T_Any_34 -> AgdaAny
du_lookup_94 :: [AgdaAny] -> T_Any_34 -> AgdaAny
du_lookup_94 [AgdaAny]
v0 T_Any_34
v1
= ([AgdaAny] -> T_Fin_6 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
[AgdaAny] -> T_Fin_6 -> AgdaAny
MAlonzo.Code.Data.List.Base.du_lookup_410 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0)
(([AgdaAny] -> T_Any_34 -> T_Fin_6) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Fin_6
du_index_86 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v1))
d__'8759''61'__102 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
[AgdaAny] -> (AgdaAny -> ()) -> T_Any_34 -> AgdaAny -> [AgdaAny]
d__'8759''61'__102 :: ()
-> ()
-> ()
-> [AgdaAny]
-> (AgdaAny -> ())
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
d__'8759''61'__102 ~()
v0 ~()
v1 ~()
v2 [AgdaAny]
v3 ~AgdaAny -> ()
v4 T_Any_34
v5 AgdaAny
v6
= [AgdaAny] -> T_Any_34 -> AgdaAny -> [AgdaAny]
du__'8759''61'__102 [AgdaAny]
v3 T_Any_34
v5 AgdaAny
v6
du__'8759''61'__102 ::
[AgdaAny] -> T_Any_34 -> AgdaAny -> [AgdaAny]
du__'8759''61'__102 :: [AgdaAny] -> T_Any_34 -> AgdaAny -> [AgdaAny]
du__'8759''61'__102 [AgdaAny]
v0 T_Any_34
v1 AgdaAny
v2
= ([AgdaAny] -> T_Fin_6 -> AgdaAny -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
[AgdaAny] -> T_Fin_6 -> AgdaAny -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du__'91'_'93''8759''61'__780 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0)
(([AgdaAny] -> T_Any_34 -> T_Fin_6) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Fin_6
du_index_86 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v1)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
d__'9472'__114 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) -> [AgdaAny] -> T_Any_34 -> [AgdaAny]
d__'9472'__114 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> [AgdaAny]
-> T_Any_34
-> [AgdaAny]
d__'9472'__114 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 [AgdaAny]
v4 T_Any_34
v5 = [AgdaAny] -> T_Any_34 -> [AgdaAny]
du__'9472'__114 [AgdaAny]
v4 T_Any_34
v5
du__'9472'__114 :: [AgdaAny] -> T_Any_34 -> [AgdaAny]
du__'9472'__114 :: [AgdaAny] -> T_Any_34 -> [AgdaAny]
du__'9472'__114 [AgdaAny]
v0 T_Any_34
v1
= ([AgdaAny] -> T_Fin_6 -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
[AgdaAny] -> T_Fin_6 -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du__'9472'__790 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0)
(([AgdaAny] -> T_Any_34 -> T_Fin_6) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Fin_6
du_index_86 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v1))
d_satisfied_120 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
[AgdaAny] -> T_Any_34 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_satisfied_120 :: ()
-> () -> () -> (AgdaAny -> ()) -> [AgdaAny] -> T_Any_34 -> T_Σ_14
d_satisfied_120 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 [AgdaAny]
v4 T_Any_34
v5 = [AgdaAny] -> T_Any_34 -> T_Σ_14
du_satisfied_120 [AgdaAny]
v4 T_Any_34
v5
du_satisfied_120 ::
[AgdaAny] -> T_Any_34 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_satisfied_120 :: [AgdaAny] -> T_Any_34 -> T_Σ_14
du_satisfied_120 [AgdaAny]
v0 T_Any_34
v1
= case T_Any_34 -> T_Any_34
forall a b. a -> b
coe T_Any_34
v1 of
C_here_46 AgdaAny
v4
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
(:) AgdaAny
v5 [AgdaAny]
v6
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
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
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
[AgdaAny]
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
C_there_54 T_Any_34
v4
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
(:) AgdaAny
v5 [AgdaAny]
v6 -> ([AgdaAny] -> T_Any_34 -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Σ_14
du_satisfied_120 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v4)
[AgdaAny]
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Any_34
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toSum_126 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] -> T_Any_34 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_toSum_126 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T__'8846'__30
d_toSum_126 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~AgdaAny
v4 ~[AgdaAny]
v5 T_Any_34
v6 = T_Any_34 -> T__'8846'__30
du_toSum_126 T_Any_34
v6
du_toSum_126 ::
T_Any_34 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_toSum_126 :: T_Any_34 -> T__'8846'__30
du_toSum_126 T_Any_34
v0
= case T_Any_34 -> T_Any_34
forall a b. a -> b
coe T_Any_34
v0 of
C_here_46 AgdaAny
v3
-> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
C_there_54 T_Any_34
v3
-> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v3)
T_Any_34
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
d_fromSum_132 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
AgdaAny ->
[AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Any_34
d_fromSum_132 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Any_34
d_fromSum_132 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~AgdaAny
v4 ~[AgdaAny]
v5 T__'8846'__30
v6 = T__'8846'__30 -> T_Any_34
du_fromSum_132 T__'8846'__30
v6
du_fromSum_132 ::
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Any_34
du_fromSum_132 :: T__'8846'__30 -> T_Any_34
du_fromSum_132 T__'8846'__30
v0
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v1 -> (AgdaAny -> T_Any_34) -> AgdaAny -> T_Any_34
forall a b. a -> b
coe AgdaAny -> T_Any_34
C_here_46 AgdaAny
v1
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v1 -> (T_Any_34 -> T_Any_34) -> AgdaAny -> T_Any_34
forall a b. a -> b
coe T_Any_34 -> T_Any_34
C_there_54 AgdaAny
v1
T__'8846'__30
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
d_any'63'_138 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_any'63'_138 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> T_Dec_32
d_any'63'_138 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 AgdaAny -> T_Dec_32
v4 [AgdaAny]
v5 = (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Dec_32
du_any'63'_138 AgdaAny -> T_Dec_32
v4 [AgdaAny]
v5
du_any'63'_138 ::
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_any'63'_138 :: (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Dec_32
du_any'63'_138 AgdaAny -> T_Dec_32
v0 [AgdaAny]
v1
= case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
[]
-> (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)
(:) AgdaAny
v2 [AgdaAny]
v3
-> ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
((T__'8846'__30 -> T_Any_34) -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> T_Any_34
du_fromSum_132)
((T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Sum.du__'8846''45'dec__32 ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v2)
(((AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Dec_32
du_any'63'_138 ((AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)))
[AgdaAny]
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_satisfiable_148 ::
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_148 :: () -> () -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14
d_satisfiable_148 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 T_Σ_14
v4 = T_Σ_14 -> T_Σ_14
du_satisfiable_148 T_Σ_14
v4
du_satisfiable_148 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_satisfiable_148 :: T_Σ_14 -> T_Σ_14
du_satisfiable_148 T_Σ_14
v0
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_298 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
((AgdaAny -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_34
C_here_46 AgdaAny
v2)
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_any_154 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_any_154 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> T_Dec_32
d_any_154 ()
v0 ()
v1 ()
v2 AgdaAny -> ()
v3 AgdaAny -> T_Dec_32
v4 [AgdaAny]
v5 = ((AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Dec_32
forall a b. a -> b
coe (AgdaAny -> T_Dec_32) -> [AgdaAny] -> T_Dec_32
du_any'63'_138 AgdaAny -> T_Dec_32
v4 [AgdaAny]
v5