{-# 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
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
d__'8712'__44 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
AgdaAny -> [AgdaAny] -> ()
d__'8712'__44 = erased
d__'8713'__46 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
AgdaAny -> [AgdaAny] -> ()
d__'8713'__46 = erased
d_find_48 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
(AgdaAny -> ()) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_find_48 ~v0 ~v1 v2 = du_find_48 v2
du_find_48 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
(AgdaAny -> ()) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_find_48 v0 v1 v2 v3 v4
= coe
MAlonzo.Code.Data.List.Membership.Setoid.du_find_80
(coe MAlonzo.Code.Relation.Binary.Bundles.du_setoid_118 (coe v0))
v3 v4
d_lose_50 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
(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_50 ~v0 ~v1 ~v2 = du_lose_50
du_lose_50 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
(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_50 v0 v1 v2 v3 v4 v5 v6
= coe
MAlonzo.Code.Data.List.Membership.Setoid.du_lose_90 v2 v3 v4 v5 v6
d_mapWith'8712'_52 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
[AgdaAny] ->
(AgdaAny ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
[AgdaAny]
d_mapWith'8712'_52 ~v0 ~v1 v2 = du_mapWith'8712'_52 v2
du_mapWith'8712'_52 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
[AgdaAny] ->
(AgdaAny ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
[AgdaAny]
du_mapWith'8712'_52 v0 v1 v2 v3 v4
= coe
MAlonzo.Code.Data.List.Membership.Setoid.du_mapWith'8712'_58
(coe MAlonzo.Code.Relation.Binary.Bundles.du_setoid_118 (coe v0))
v3 v4
d__'8759''61'__56 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
[AgdaAny] ->
(AgdaAny -> ()) ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
AgdaAny -> [AgdaAny]
d__'8759''61'__56 ~v0 = du__'8759''61'__56
du__'8759''61'__56 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
[AgdaAny] ->
(AgdaAny -> ()) ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
AgdaAny -> [AgdaAny]
du__'8759''61'__56 v0 v1 v2 v3 v4 v5 v6
= coe
MAlonzo.Code.Data.List.Relation.Unary.Any.du__'8759''61'__102 v3 v5
v6
d__'9472'__58 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
(AgdaAny -> ()) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> [AgdaAny]
d__'9472'__58 ~v0 = du__'9472'__58
du__'9472'__58 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
(AgdaAny -> ()) ->
[AgdaAny] ->
MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> [AgdaAny]
du__'9472'__58 v0 v1 v2 v3 v4 v5
= coe
MAlonzo.Code.Data.List.Relation.Unary.Any.du__'9472'__114 v4 v5
d__'8712''63'__60 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
AgdaAny -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8712''63'__60 ~v0 ~v1 v2 v3 v4 = du__'8712''63'__60 v2 v3 v4
du__'8712''63'__60 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
AgdaAny -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8712''63'__60 v0 v1 v2
= coe
MAlonzo.Code.Data.List.Relation.Unary.Any.du_any'63'_138
(coe
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52
(MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
(coe v0))
v1)
(coe v2)
d__'8713''63'__68 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
AgdaAny -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8713''63'__68 ~v0 ~v1 v2 v3 v4 = du__'8713''63'__68 v2 v3 v4
du__'8713''63'__68 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
AgdaAny -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8713''63'__68 v0 v1 v2
= coe
MAlonzo.Code.Relation.Nullary.Negation.Core.du_'172''63'_64
(coe du__'8712''63'__60 (coe v0) (coe v1) (coe v2))