{-# 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.Relation.Nullary.Decidable 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Relation.Nullary.Decidable.map
d_map_18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_map_18 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1714
-> T_Dec_20
-> T_Dec_20
d_map_18 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Equivalence_1714
v4 = T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20
du_map_18 T_Equivalence_1714
v4
du_map_18 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_map_18 :: T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20
du_map_18 T_Equivalence_1714
v0
  = ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> Any -> T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
      ((T_Equivalence_1714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1724 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v0))
      ((T_Equivalence_1714 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1714 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1726 (T_Equivalence_1714 -> Any
forall a b. a -> b
coe T_Equivalence_1714
v0))
-- Relation.Nullary.Decidable._.Eq₁._≈_
d__'8776'__114 ::
  T_GeneralizeTel_1875 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__114 :: T_GeneralizeTel_1875
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_776
-> Any
-> Any
-> T_Level_18
d__'8776'__114 = T_GeneralizeTel_1875
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_776
-> Any
-> Any
-> T_Level_18
forall a. a
erased
-- Relation.Nullary.Decidable._.Eq₂._≈_
d__'8776'__138 ::
  T_GeneralizeTel_1875 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__138 :: T_GeneralizeTel_1875
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_776
-> Any
-> Any
-> T_Level_18
d__'8776'__138 = T_GeneralizeTel_1875
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_776
-> Any
-> Any
-> T_Level_18
forall a. a
erased
-- Relation.Nullary.Decidable.via-injection
d_via'45'injection_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_via'45'injection_160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_776
-> (Any -> Any -> T_Dec_20)
-> Any
-> Any
-> T_Dec_20
d_via'45'injection_160 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Injection_776
v6 Any -> Any -> T_Dec_20
v7 Any
v8 Any
v9
  = T_Injection_776
-> (Any -> Any -> T_Dec_20) -> Any -> Any -> T_Dec_20
du_via'45'injection_160 T_Injection_776
v6 Any -> Any -> T_Dec_20
v7 Any
v8 Any
v9
du_via'45'injection_160 ::
  MAlonzo.Code.Function.Bundles.T_Injection_776 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_via'45'injection_160 :: T_Injection_776
-> (Any -> Any -> T_Dec_20) -> Any -> Any -> T_Dec_20
du_via'45'injection_160 T_Injection_776
v0 Any -> Any -> T_Dec_20
v1 Any
v2 Any
v3
  = ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
      ((T_Injection_776 -> Any -> Any -> Any -> Any)
-> T_Injection_776 -> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_injective_788 T_Injection_776
v0 Any
v2 Any
v3)
      ((T_Injection_776 -> Any -> Any -> Any -> Any)
-> T_Injection_776 -> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_786 T_Injection_776
v0 Any
v2 Any
v3)
      ((Any -> Any -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Dec_20
v1 ((T_Injection_776 -> Any -> Any) -> T_Injection_776 -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_784 T_Injection_776
v0 Any
v2)
         ((T_Injection_776 -> Any -> Any) -> T_Injection_776 -> Any -> Any
forall a b. a -> b
coe T_Injection_776 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_784 T_Injection_776
v0 Any
v3))
-- Relation.Nullary.Decidable.True-↔
d_True'45''8596'_238 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_True'45''8596'_238 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> T_Inverse_1960
d_True'45''8596'_238 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_20
v2 ~Any -> Any -> T__'8801'__12
v3 = T_Dec_20 -> T_Inverse_1960
du_True'45''8596'_238 T_Dec_20
v2
du_True'45''8596'_238 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_True'45''8596'_238 :: T_Dec_20 -> T_Inverse_1960
du_True'45''8596'_238 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then ((Any -> Any) -> (Any -> Any) -> T_Inverse_1960)
-> Any -> Any -> T_Inverse_1960
forall a b. a -> b
coe
                    (Any -> Any) -> (Any -> Any) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
                    ((Any -> Any) -> Any
forall a b. a -> b
coe
                       (\ Any
v3 ->
                          (T_Reflects_16 -> Any) -> Any -> Any
forall a b. a -> b
coe T_Reflects_16 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v2)))
                    ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v3 -> T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
             else ((Any -> Any) -> (Any -> Any) -> T_Inverse_1960)
-> Any -> Any -> T_Inverse_1960
forall a b. a -> b
coe
                    (Any -> Any) -> (Any -> Any) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366 Any
forall a. a
erased
                    ((T_Reflects_16 -> Any) -> Any -> Any
forall a b. a -> b
coe T_Reflects_16 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v2))
      T_Dec_20
_ -> T_Inverse_1960
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.isYes≗does
d_isYes'8791'does_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_isYes'8791'does_256 :: T_Level_18 -> T_Level_18 -> T_Dec_20 -> T__'8801'__12
d_isYes'8791'does_256 = T_Level_18 -> T_Level_18 -> T_Dec_20 -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-true
d_dec'45'true_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'true_260 :: T_Level_18 -> T_Level_18 -> T_Dec_20 -> Any -> T__'8801'__12
d_dec'45'true_260 = T_Level_18 -> T_Level_18 -> T_Dec_20 -> Any -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-false
d_dec'45'false_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'false_270 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> T_Irrelevant_20)
-> T__'8801'__12
d_dec'45'false_270 = T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> T_Irrelevant_20)
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-yes
d_dec'45'yes_282 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_dec'45'yes_282 :: T_Level_18 -> T_Level_18 -> T_Dec_20 -> Any -> T_Σ_14
d_dec'45'yes_282 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_20
v2 ~Any
v3 = T_Dec_20 -> T_Σ_14
du_dec'45'yes_282 T_Dec_20
v2
du_dec'45'yes_282 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_dec'45'yes_282 :: T_Dec_20 -> T_Σ_14
du_dec'45'yes_282 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v1 T_Reflects_16
v2
        -> (Any -> Any -> Any) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
             Any -> Any -> Any
forall a b. a -> b -> b
seq (Bool -> Any
forall a b. a -> b
coe Bool
v1)
             (case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2 of
                MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v3
                  -> (Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (Any -> Any
forall a b. a -> b
coe Any
v3) Any
forall a. a
erased
                T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
      T_Dec_20
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.dec-no
d_dec'45'no_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'no_298 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> T_Irrelevant_20)
-> T__'8801'__12
d_dec'45'no_298 = T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> T_Irrelevant_20)
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-yes-irr
d_dec'45'yes'45'irr_312 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'yes'45'irr_312 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> Any
-> T__'8801'__12
d_dec'45'yes'45'irr_312 = T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> Any
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.⌊⌋-map′
d_'8970''8971''45'map'8242'_338 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8970''8971''45'map'8242'_338 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> (Any -> Any)
-> T_Dec_20
-> T__'8801'__12
d_'8970''8971''45'map'8242'_338 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> (Any -> Any)
-> T_Dec_20
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable..generalizedField-a
d_'46'generalizedField'45'a_1867 ::
  T_GeneralizeTel_1875 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'a_1867 :: T_GeneralizeTel_1875 -> T_Level_18
d_'46'generalizedField'45'a_1867 T_GeneralizeTel_1875
v0
  = case T_GeneralizeTel_1875 -> T_GeneralizeTel_1875
forall a b. a -> b
coe T_GeneralizeTel_1875
v0 of
      C_mkGeneralizeTel_1877 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_Level_18
v4 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v1
      T_GeneralizeTel_1875
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable..generalizedField-ℓ₁
d_'46'generalizedField'45'ℓ'8321'_1869 ::
  T_GeneralizeTel_1875 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'ℓ'8321'_1869 :: T_GeneralizeTel_1875 -> T_Level_18
d_'46'generalizedField'45'ℓ'8321'_1869 T_GeneralizeTel_1875
v0
  = case T_GeneralizeTel_1875 -> T_GeneralizeTel_1875
forall a b. a -> b
coe T_GeneralizeTel_1875
v0 of
      C_mkGeneralizeTel_1877 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_Level_18
v4 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v2
      T_GeneralizeTel_1875
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable..generalizedField-b
d_'46'generalizedField'45'b_1871 ::
  T_GeneralizeTel_1875 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'b_1871 :: T_GeneralizeTel_1875 -> T_Level_18
d_'46'generalizedField'45'b_1871 T_GeneralizeTel_1875
v0
  = case T_GeneralizeTel_1875 -> T_GeneralizeTel_1875
forall a b. a -> b
coe T_GeneralizeTel_1875
v0 of
      C_mkGeneralizeTel_1877 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_Level_18
v4 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v3
      T_GeneralizeTel_1875
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable..generalizedField-ℓ₂
d_'46'generalizedField'45'ℓ'8322'_1873 ::
  T_GeneralizeTel_1875 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'ℓ'8322'_1873 :: T_GeneralizeTel_1875 -> T_Level_18
d_'46'generalizedField'45'ℓ'8322'_1873 T_GeneralizeTel_1875
v0
  = case T_GeneralizeTel_1875 -> T_GeneralizeTel_1875
forall a b. a -> b
coe T_GeneralizeTel_1875
v0 of
      C_mkGeneralizeTel_1877 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_Level_18
v4 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v4
      T_GeneralizeTel_1875
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.GeneralizeTel
d_GeneralizeTel_1875 :: T_Level_18
d_GeneralizeTel_1875 = ()
data T_GeneralizeTel_1875
  = C_mkGeneralizeTel_1877 MAlonzo.Code.Agda.Primitive.T_Level_18
                           MAlonzo.Code.Agda.Primitive.T_Level_18
                           MAlonzo.Code.Agda.Primitive.T_Level_18
                           MAlonzo.Code.Agda.Primitive.T_Level_18