{-# 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.Membership.Setoid 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.List
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.List.Relation.Unary.Any
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Data.List.Membership.Setoid._∈_
d__'8712'__36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny -> [AgdaAny] -> ()
d__'8712'__36 :: T_Level_18
-> T_Level_18 -> T_Setoid_44 -> AgdaAny -> [AgdaAny] -> T_Level_18
d__'8712'__36 = T_Level_18
-> T_Level_18 -> T_Setoid_44 -> AgdaAny -> [AgdaAny] -> T_Level_18
forall a. a
erased
-- Data.List.Membership.Setoid._∉_
d__'8713'__44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  AgdaAny -> [AgdaAny] -> ()
d__'8713'__44 :: T_Level_18
-> T_Level_18 -> T_Setoid_44 -> AgdaAny -> [AgdaAny] -> T_Level_18
d__'8713'__44 = T_Level_18
-> T_Level_18 -> T_Setoid_44 -> AgdaAny -> [AgdaAny] -> T_Level_18
forall a. a
erased
-- Data.List.Membership.Setoid._∷=_
d__'8759''61'__50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  [AgdaAny] ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny -> [AgdaAny]
d__'8759''61'__50 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
d__'8759''61'__50 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
du__'8759''61'__50
du__'8759''61'__50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  [AgdaAny] ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny -> [AgdaAny]
du__'8759''61'__50 :: T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
du__'8759''61'__50 T_Level_18
v0 [AgdaAny]
v1 AgdaAny -> T_Level_18
v2 T_Any_34
v3 AgdaAny
v4
  = ([AgdaAny] -> T_Any_34 -> AgdaAny -> [AgdaAny])
-> [AgdaAny] -> T_Any_34 -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
      [AgdaAny] -> T_Any_34 -> AgdaAny -> [AgdaAny]
MAlonzo.Code.Data.List.Relation.Unary.Any.du__'8759''61'__102 [AgdaAny]
v1 T_Any_34
v3
      AgdaAny
v4
-- Data.List.Membership.Setoid._─_
d__'9472'__52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> [AgdaAny]
d__'9472'__52 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> [AgdaAny]
d__'9472'__52 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 = T_Level_18
-> (AgdaAny -> T_Level_18) -> [AgdaAny] -> T_Any_34 -> [AgdaAny]
du__'9472'__52
du__'9472'__52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> [AgdaAny]
du__'9472'__52 :: T_Level_18
-> (AgdaAny -> T_Level_18) -> [AgdaAny] -> T_Any_34 -> [AgdaAny]
du__'9472'__52 T_Level_18
v0 AgdaAny -> T_Level_18
v1 [AgdaAny]
v2 T_Any_34
v3
  = ([AgdaAny] -> T_Any_34 -> [AgdaAny])
-> [AgdaAny] -> T_Any_34 -> [AgdaAny]
forall a b. a -> b
coe
      [AgdaAny] -> T_Any_34 -> [AgdaAny]
MAlonzo.Code.Data.List.Relation.Unary.Any.du__'9472'__114 [AgdaAny]
v2 T_Any_34
v3
-- Data.List.Membership.Setoid.mapWith∈
d_mapWith'8712'_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
  [AgdaAny]
d_mapWith'8712'_62 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
d_mapWith'8712'_62 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 ~T_Level_18
v3 ~T_Level_18
v4 [AgdaAny]
v5 AgdaAny -> T_Any_34 -> AgdaAny
v6
  = T_Setoid_44
-> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny]
du_mapWith'8712'_62 T_Setoid_44
v2 [AgdaAny]
v5 AgdaAny -> T_Any_34 -> AgdaAny
v6
du_mapWith'8712'_62 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
  [AgdaAny]
du_mapWith'8712'_62 :: T_Setoid_44
-> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny]
du_mapWith'8712'_62 T_Setoid_44
v0 [AgdaAny]
v1 AgdaAny -> T_Any_34 -> AgdaAny
v2
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
      [] -> [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1
      (:) AgdaAny
v3 [AgdaAny]
v4
        -> (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
             AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
             ((AgdaAny -> T_Any_34 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T_Any_34 -> AgdaAny
v2 AgdaAny
v3
                ((AgdaAny -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46
                   ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                      (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                      AgdaAny
v3)))
             ((T_Setoid_44
 -> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Setoid_44
-> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny]
du_mapWith'8712'_62 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4)
                ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                   (\ AgdaAny
v5 AgdaAny
v6 ->
                      (AgdaAny -> T_Any_34 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        AgdaAny -> T_Any_34 -> AgdaAny
v2 AgdaAny
v5
                        ((T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 AgdaAny
v6))))
      [AgdaAny]
_ -> [AgdaAny]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Membership.Setoid._.find
d_find_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_find_84 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T_Σ_14
d_find_84 ~T_Level_18
v0 ~T_Level_18
v1 T_Setoid_44
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 [AgdaAny]
v5 T_Any_34
v6 = T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
du_find_84 T_Setoid_44
v2 [AgdaAny]
v5 T_Any_34
v6
du_find_84 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_find_84 :: T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
du_find_84 T_Setoid_44
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
      MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 AgdaAny
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> (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
v6)
                    ((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 -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46
                          ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                             (T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
                             AgdaAny
v6))
                       (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
             [AgdaAny]
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 T_Any_34
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> (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
                    ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                       ((T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
du_find_84 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
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 -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                       ((T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54
                          (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                             ((T_Σ_14 -> AgdaAny) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                                T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                                ((T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
du_find_84 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
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)))))
                       ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                          ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                             ((T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
du_find_84 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
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_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Any_34
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Membership.Setoid._.lose
d_lose_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny -> MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
d_lose_100 :: T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> AgdaAny
-> T_Any_34
d_lose_100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Setoid_44
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 [AgdaAny]
v7 T_Any_34
v8 AgdaAny
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
du_lose_100 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v5 AgdaAny
v6 [AgdaAny]
v7 T_Any_34
v8 AgdaAny
v9
du_lose_100 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny -> MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
du_lose_100 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
du_lose_100 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 [AgdaAny]
v2 T_Any_34
v3 AgdaAny
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_Any_34 -> T_Any_34)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Any_34
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.du_map_76
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v5 AgdaAny
v6 AgdaAny
v4)) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2) (T_Any_34 -> AgdaAny
forall a b. a -> b
coe T_Any_34
v3)