{-# 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.DecSetoid 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.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
d__'8712'__46 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
AgdaAny -> [AgdaAny] -> ()
d__'8712'__46 :: T_Level_18
-> T_Level_18
-> T_DecSetoid_90
-> AgdaAny
-> [AgdaAny]
-> T_Level_18
d__'8712'__46 = T_Level_18
-> T_Level_18
-> T_DecSetoid_90
-> AgdaAny
-> [AgdaAny]
-> T_Level_18
forall a. a
erased
d__'8713'__48 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
AgdaAny -> [AgdaAny] -> ()
d__'8713'__48 :: T_Level_18
-> T_Level_18
-> T_DecSetoid_90
-> AgdaAny
-> [AgdaAny]
-> T_Level_18
d__'8713'__48 = T_Level_18
-> T_Level_18
-> T_DecSetoid_90
-> AgdaAny
-> [AgdaAny]
-> T_Level_18
forall a. a
erased
d__'8759''61'__50 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
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_DecSetoid_90
-> 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_DecSetoid_90
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
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny])
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
forall a b. a -> b
coe T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
MAlonzo.Code.Data.List.Membership.Setoid.du__'8759''61'__52
d__'9472'__52 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
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_DecSetoid_90
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> [AgdaAny]
d__'9472'__52 ~T_Level_18
v0 ~T_Level_18
v1 ~T_DecSetoid_90
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
-> (AgdaAny -> T_Level_18) -> [AgdaAny] -> T_Any_34 -> [AgdaAny])
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> [AgdaAny]
forall a b. a -> b
coe T_Level_18
-> (AgdaAny -> T_Level_18) -> [AgdaAny] -> T_Any_34 -> [AgdaAny]
MAlonzo.Code.Data.List.Membership.Setoid.du__'9472'__54
d_find_54 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
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_54 :: T_Level_18
-> T_Level_18
-> T_DecSetoid_90
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T_Σ_14
d_find_54 ~T_Level_18
v0 ~T_Level_18
v1 T_DecSetoid_90
v2 = T_DecSetoid_90
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T_Σ_14
du_find_54 T_DecSetoid_90
v2
du_find_54 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
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_54 :: T_DecSetoid_90
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T_Σ_14
du_find_54 T_DecSetoid_90
v0 T_Level_18
v1 AgdaAny -> T_Level_18
v2 [AgdaAny]
v3 T_Any_34
v4
= (T_Setoid_46 -> [AgdaAny] -> T_Any_34 -> T_Σ_14)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> T_Σ_14
forall a b. a -> b
coe
T_Setoid_46 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
MAlonzo.Code.Data.List.Membership.Setoid.du_find_86
((T_DecSetoid_90 -> T_Setoid_46) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.du_setoid_114 (T_DecSetoid_90 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90
v0))
[AgdaAny]
v3 T_Any_34
v4
d_lose_56 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
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_56 :: T_Level_18
-> T_Level_18
-> T_DecSetoid_90
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> AgdaAny
-> T_Any_34
d_lose_56 ~T_Level_18
v0 ~T_Level_18
v1 ~T_DecSetoid_90
v2 = T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> AgdaAny
-> T_Any_34
du_lose_56
du_lose_56 ::
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
du_lose_56 :: T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> AgdaAny
-> T_Any_34
du_lose_56 T_Level_18
v0 AgdaAny -> T_Level_18
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 [AgdaAny]
v4 T_Any_34
v5 AgdaAny
v6
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> 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_102 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 [AgdaAny]
v4 T_Any_34
v5 AgdaAny
v6
d_mapWith'8712'_58 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[AgdaAny] ->
(AgdaAny ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
[AgdaAny]
d_mapWith'8712'_58 :: T_Level_18
-> T_Level_18
-> T_DecSetoid_90
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
d_mapWith'8712'_58 ~T_Level_18
v0 ~T_Level_18
v1 T_DecSetoid_90
v2 = T_DecSetoid_90
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
du_mapWith'8712'_58 T_DecSetoid_90
v2
du_mapWith'8712'_58 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[AgdaAny] ->
(AgdaAny ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
[AgdaAny]
du_mapWith'8712'_58 :: T_DecSetoid_90
-> T_Level_18
-> T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
du_mapWith'8712'_58 T_DecSetoid_90
v0 T_Level_18
v1 T_Level_18
v2 [AgdaAny]
v3 AgdaAny -> T_Any_34 -> AgdaAny
v4
= (T_Setoid_46
-> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny])
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
forall a b. a -> b
coe
T_Setoid_46
-> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny]
MAlonzo.Code.Data.List.Membership.Setoid.du_mapWith'8712'_64
((T_DecSetoid_90 -> T_Setoid_46) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.du_setoid_114 (T_DecSetoid_90 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90
v0))
[AgdaAny]
v3 AgdaAny -> T_Any_34 -> AgdaAny
v4
d__'8712''63'__60 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
AgdaAny ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8712''63'__60 :: T_Level_18
-> T_Level_18 -> T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
d__'8712''63'__60 ~T_Level_18
v0 ~T_Level_18
v1 T_DecSetoid_90
v2 AgdaAny
v3 [AgdaAny]
v4 = T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
du__'8712''63'__60 T_DecSetoid_90
v2 AgdaAny
v3 [AgdaAny]
v4
du__'8712''63'__60 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
AgdaAny ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'8712''63'__60 :: T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
du__'8712''63'__60 T_DecSetoid_90
v0 AgdaAny
v1 [AgdaAny]
v2
= ((AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Unary.Any.du_any'63'_138
((T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsDecEquivalence_48 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__56
(T_DecSetoid_90 -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_106
(T_DecSetoid_90 -> T_DecSetoid_90
forall a b. a -> b
coe T_DecSetoid_90
v0))
AgdaAny
v1)
([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
d__'8713''63'__68 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
AgdaAny ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8713''63'__68 :: T_Level_18
-> T_Level_18 -> T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
d__'8713''63'__68 ~T_Level_18
v0 ~T_Level_18
v1 T_DecSetoid_90
v2 AgdaAny
v3 [AgdaAny]
v4 = T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
du__'8713''63'__68 T_DecSetoid_90
v2 AgdaAny
v3 [AgdaAny]
v4
du__'8713''63'__68 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90 ->
AgdaAny ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'8713''63'__68 :: T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
du__'8713''63'__68 T_DecSetoid_90
v0 AgdaAny
v1 [AgdaAny]
v2
= (T_Dec_20 -> T_Dec_20) -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_'172''63'_76
((T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
du__'8712''63'__60 (T_DecSetoid_90 -> AgdaAny
forall a b. a -> b
coe T_DecSetoid_90
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2))