{-# 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

-- Data.List.Relation.Unary.Any.Any
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
-- Data.List.Relation.Unary.Any.head
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
-- Data.List.Relation.Unary.Any.tail
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
-- Data.List.Relation.Unary.Any.map
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
-- Data.List.Relation.Unary.Any.index
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
-- Data.List.Relation.Unary.Any.lookup
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))
-- Data.List.Relation.Unary.Any._∷=_
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)
-- Data.List.Relation.Unary.Any._─_
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))
-- Data.List.Relation.Unary.Any.satisfied
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
-- Data.List.Relation.Unary.Any.toSum
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
-- Data.List.Relation.Unary.Any.fromSum
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
-- Data.List.Relation.Unary.Any.any?
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
-- Data.List.Relation.Unary.Any.satisfiable
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
-- Data.List.Relation.Unary.Any.any
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