{-# 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.Fin.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
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.Irrelevant.T_Irrelevant_20) ->
T_Any_34 -> AgdaAny
d_head_56 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> [AgdaAny]
-> AgdaAny
-> (T_Any_34 -> T_Irrelevant_20)
-> T_Any_34
-> AgdaAny
d_head_56 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~[AgdaAny]
v4 ~AgdaAny
v5 ~T_Any_34 -> T_Irrelevant_20
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 -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
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.Irrelevant.T_Irrelevant_20) ->
T_Any_34 -> T_Any_34
d_tail_66 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_Irrelevant_20)
-> T_Any_34
-> T_Any_34
d_tail_66 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~AgdaAny
v4 ~[AgdaAny]
v5 ~AgdaAny -> T_Irrelevant_20
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_Irrelevant_20) -> AgdaAny) -> AgdaAny -> T_Any_34
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
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_10
d_index_86 :: ()
-> () -> () -> (AgdaAny -> ()) -> [AgdaAny] -> T_Any_34 -> T_Fin_10
d_index_86 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 [AgdaAny]
v4 T_Any_34
v5 = [AgdaAny] -> T_Any_34 -> T_Fin_10
du_index_86 [AgdaAny]
v4 T_Any_34
v5
du_index_86 ::
[AgdaAny] -> T_Any_34 -> MAlonzo.Code.Data.Fin.Base.T_Fin_10
du_index_86 :: [AgdaAny] -> T_Any_34 -> T_Fin_10
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_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
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_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(([AgdaAny] -> T_Any_34 -> T_Fin_10)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Fin_10
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_10
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Any_34
_ -> T_Fin_10
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_10 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
[AgdaAny] -> T_Fin_10 -> AgdaAny
MAlonzo.Code.Data.List.Base.du_lookup_406 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0)
(([AgdaAny] -> T_Any_34 -> T_Fin_10)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Fin_10
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_10 -> AgdaAny -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
[AgdaAny] -> T_Fin_10 -> AgdaAny -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du__'91'_'93''8759''61'__986 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0)
(([AgdaAny] -> T_Any_34 -> T_Fin_10)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Fin_10
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_10 -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
[AgdaAny] -> T_Fin_10 -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_removeAt_586 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0)
(([AgdaAny] -> T_Any_34 -> T_Fin_10)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Any_34 -> T_Fin_10
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.Decidable.Core.T_Dec_20) ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_any'63'_138 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> T_Dec_20
d_any'63'_138 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 AgdaAny -> T_Dec_20
v4 [AgdaAny]
v5 = (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20
du_any'63'_138 AgdaAny -> T_Dec_20
v4 [AgdaAny]
v5
du_any'63'_138 ::
(AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_any'63'_138 :: (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20
du_any'63'_138 AgdaAny -> T_Dec_20
v0 [AgdaAny]
v1
= case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
[]
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
(:) AgdaAny
v2 [AgdaAny]
v3
-> ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
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_Any_34 -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe T_Any_34 -> T__'8846'__30
du_toSum_126)
((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'8846''45'dec__86
((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v2) (((AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20
du_any'63'_138 ((AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)))
[AgdaAny]
_ -> T_Dec_20
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'_286 (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.Decidable.Core.T_Dec_20) ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_any_154 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> T_Dec_20
d_any_154 ()
v0 ()
v1 ()
v2 AgdaAny -> ()
v3 AgdaAny -> T_Dec_20
v4 [AgdaAny]
v5 = ((AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20)
-> (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20
forall a b. a -> b
coe (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20
du_any'63'_138 AgdaAny -> T_Dec_20
v4 [AgdaAny]
v5