content: {-# 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 Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.List qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.List.Relation.Unary.Any qualified
  import MAlonzo.Code.Relation.Binary.Bundles qualified
  import MAlonzo.Code.Relation.Binary.Structures qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- 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 = 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 = 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 ~v0 ~v1 ~v2 = 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 v0 v1 v2 v3 v4
    = coe
        MAlonzo.Code.Data.List.Relation.Unary.Any.du__'8759''61'__102 v1 v3
        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 ~v0 ~v1 ~v2 = 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 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Data.List.Relation.Unary.Any.du__'9472'__114 v2 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 ~v0 ~v1 v2 ~v3 ~v4 v5 v6
    = du_mapWith'8712'_62 v2 v5 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 v0 v1 v2
    = case coe v1 of
        [] -> coe v1
        (:) v3 v4
          -> coe
               MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
               (coe
                  v2 v3
                  (coe
                     MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46
                     (coe
                        MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                        (MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))
                        v3)))
               (coe
                  du_mapWith'8712'_62 (coe v0) (coe v4)
                  (coe
                     (\ v5 v6 ->
                        coe
                          v2 v5
                          (coe MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v6))))
        _ -> 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 ~v0 ~v1 v2 ~v3 ~v4 v5 v6 = du_find_84 v2 v5 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 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 v5
          -> case coe v1 of
               (:) v6 v7
                 -> coe
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v6)
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         (coe
                            MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46
                            (coe
                               MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                               (MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))
                               v6))
                         (coe v5))
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v5
          -> case coe v1 of
               (:) v6 v7
                 -> coe
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                         (coe du_find_84 (coe v0) (coe v7) (coe v5)))
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         (coe
                            MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54
                            (MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                               (coe
                                  MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                                  (coe du_find_84 (coe v0) (coe v7) (coe v5)))))
                         (coe
                            MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                            (coe
                               MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                               (coe du_find_84 (coe v0) (coe v7) (coe v5)))))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> 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 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6 v7 v8 v9
    = du_lose_100 v5 v6 v7 v8 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 v0 v1 v2 v3 v4
    = coe
        MAlonzo.Code.Data.List.Relation.Unary.Any.du_map_76
        (coe (\ v5 v6 -> coe v0 v1 v5 v6 v4)) (coe v2) (coe v3)
  