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

-- Data.List.Membership.Propositional._._∈_
d__'8712'__14 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> AgdaAny -> [AgdaAny] -> ()
d__'8712'__14 :: T_Level_18 -> T_Level_18 -> AgdaAny -> [AgdaAny] -> T_Level_18
d__'8712'__14 = T_Level_18 -> T_Level_18 -> AgdaAny -> [AgdaAny] -> T_Level_18
forall a. a
erased
-- Data.List.Membership.Propositional._._∉_
d__'8713'__16 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> AgdaAny -> [AgdaAny] -> ()
d__'8713'__16 :: T_Level_18 -> T_Level_18 -> AgdaAny -> [AgdaAny] -> T_Level_18
d__'8713'__16 = T_Level_18 -> T_Level_18 -> AgdaAny -> [AgdaAny] -> T_Level_18
forall a. a
erased
-- Data.List.Membership.Propositional._.find
d_find_18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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_18 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T_Σ_14
d_find_18 ~T_Level_18
v0 ~T_Level_18
v1 = T_Level_18
-> (AgdaAny -> T_Level_18) -> [AgdaAny] -> T_Any_34 -> T_Σ_14
du_find_18
du_find_18 ::
  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
du_find_18 :: T_Level_18
-> (AgdaAny -> T_Level_18) -> [AgdaAny] -> T_Any_34 -> T_Σ_14
du_find_18 T_Level_18
v0 AgdaAny -> T_Level_18
v1 [AgdaAny]
v2 T_Any_34
v3
  = (T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> T_Σ_14
forall a b. a -> b
coe
      T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
MAlonzo.Code.Data.List.Membership.Setoid.du_find_80
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
      [AgdaAny]
v2 T_Any_34
v3
-- Data.List.Membership.Propositional._.map-with-∈
d_map'45'with'45''8712'_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
  [AgdaAny]
d_map'45'with'45''8712'_20 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
d_map'45'with'45''8712'_20 ~T_Level_18
v0 ~T_Level_18
v1 = T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
du_map'45'with'45''8712'_20
du_map'45'with'45''8712'_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
  [AgdaAny]
du_map'45'with'45''8712'_20 :: T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
du_map'45'with'45''8712'_20
  = (T_Setoid_44
 -> T_Level_18
 -> T_Level_18
 -> [AgdaAny]
 -> (AgdaAny -> T_Any_34 -> AgdaAny)
 -> [AgdaAny])
-> AgdaAny
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
forall a b. a -> b
coe
      T_Setoid_44
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
MAlonzo.Code.Data.List.Membership.Setoid.du_map'45'with'45''8712'_98
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
-- Data.List.Membership.Propositional._.mapWith∈
d_mapWith'8712'_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
  [AgdaAny]
d_mapWith'8712'_22 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
d_mapWith'8712'_22 ~T_Level_18
v0 ~T_Level_18
v1 = T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
du_mapWith'8712'_22
du_mapWith'8712'_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [AgdaAny] ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
  [AgdaAny]
du_mapWith'8712'_22 :: T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
du_mapWith'8712'_22 T_Level_18
v0 T_Level_18
v1 [AgdaAny]
v2 AgdaAny -> T_Any_34 -> AgdaAny
v3
  = (T_Setoid_44
 -> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny])
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
forall a b. a -> b
coe
      T_Setoid_44
-> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny]
MAlonzo.Code.Data.List.Membership.Setoid.du_mapWith'8712'_58
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
      [AgdaAny]
v2 AgdaAny -> T_Any_34 -> AgdaAny
v3
-- Data.List.Membership.Propositional._.Any._∷=_
d__'8759''61'__26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  [AgdaAny] ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny -> [AgdaAny]
d__'8759''61'__26 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
d__'8759''61'__26 ~T_Level_18
v0 ~T_Level_18
v1 = T_Level_18
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
du__'8759''61'__26
du__'8759''61'__26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  [AgdaAny] ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny -> [AgdaAny]
du__'8759''61'__26 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
du__'8759''61'__26 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 [AgdaAny]
v3 AgdaAny -> T_Level_18
v4 T_Any_34
v5 AgdaAny
v6
  = ([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]
v3 T_Any_34
v5
      AgdaAny
v6
-- Data.List.Membership.Propositional._.Any._─_
d__'9472'__28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> [AgdaAny]
d__'9472'__28 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> [AgdaAny]
d__'9472'__28 ~T_Level_18
v0 ~T_Level_18
v1 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> [AgdaAny]
du__'9472'__28
du__'9472'__28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> [AgdaAny]
du__'9472'__28 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> [AgdaAny]
du__'9472'__28 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 AgdaAny -> T_Level_18
v3 [AgdaAny]
v4 T_Any_34
v5
  = ([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]
v4 T_Any_34
v5
-- Data.List.Membership.Propositional._≢∈_
d__'8802''8712'__36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> ()
d__'8802''8712'__36 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_Any_34
-> T_Level_18
d__'8802''8712'__36 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_Any_34
-> T_Level_18
forall a. a
erased
-- Data.List.Membership.Propositional.lose
d_lose_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (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_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> AgdaAny
-> T_Any_34
d_lose_54 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 AgdaAny
v4 [AgdaAny]
v5 = AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
du_lose_54 AgdaAny
v4 [AgdaAny]
v5
du_lose_54 ::
  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_54 :: AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
du_lose_54 AgdaAny
v0 [AgdaAny]
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Any_34 -> AgdaAny -> T_Any_34
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Setoid.du_lose_90
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 -> AgdaAny
v5)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)