{-# 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.Core 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Level
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Relation.Nullary.Decidable.Core.Dec
d_Dec_20 :: p -> p -> ()
d_Dec_20 p
a0 p
a1 = ()
data T_Dec_20
  = C__because__32 Bool
                   MAlonzo.Code.Relation.Nullary.Reflects.T_Reflects_16
-- Relation.Nullary.Decidable.Core.Dec.does
d_does_28 :: T_Dec_20 -> Bool
d_does_28 :: T_Dec_20 -> Bool
d_does_28 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2 -> Bool -> Bool
forall a b. a -> b
coe Bool
v1
      T_Dec_20
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.Dec.proof
d_proof_30 ::
  T_Dec_20 -> MAlonzo.Code.Relation.Nullary.Reflects.T_Reflects_16
d_proof_30 :: T_Dec_20 -> T_Reflects_16
d_proof_30 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2 -> T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2
      T_Dec_20
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core._.From-yes
d_From'45'yes_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_From'45'yes_50 :: () -> () -> T_Dec_20 -> ()
d_From'45'yes_50 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
-- Relation.Nullary.Decidable.Core._.From-no
d_From'45'no_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_From'45'no_52 :: () -> () -> T_Dec_20 -> ()
d_From'45'no_52 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
-- Relation.Nullary.Decidable.Core.recompute
d_recompute_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_recompute_54 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_recompute_54 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny -> AgdaAny
du_recompute_54 T_Dec_20
v2
du_recompute_54 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_recompute_54 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_recompute_54 T_Dec_20
v0 AgdaAny
v1
  = (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_recompute_46
      ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
-- Relation.Nullary.Decidable.Core.recompute-constant
d_recompute'45'constant_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Dec_20 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_recompute'45'constant_62 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T__'8801'__12
d_recompute'45'constant_62 = () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.Core.T?
d_T'63'_66 :: Bool -> T_Dec_20
d_T'63'_66 :: Bool -> T_Dec_20
d_T'63'_66 Bool
v0
  = (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
C__because__32 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0)
      ((Bool -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
-- Relation.Nullary.Decidable.Core.¬?
d_'172''63'_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> T_Dec_20
d_'172''63'_70 :: () -> () -> T_Dec_20 -> T_Dec_20
d_'172''63'_70 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> T_Dec_20
du_'172''63'_70 T_Dec_20
v2
du_'172''63'_70 :: T_Dec_20 -> T_Dec_20
du_'172''63'_70 :: T_Dec_20 -> T_Dec_20
du_'172''63'_70 T_Dec_20
v0
  = (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
C__because__32
      ((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0)))
      ((T_Reflects_16 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Reflects_16 -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du_'172''45'reflects_70
         ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0)))
-- Relation.Nullary.Decidable.Core._×-dec_
d__'215''45'dec__76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'215''45'dec__76 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'215''45'dec__76 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Dec_20
v4 T_Dec_20
v5
  = T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'215''45'dec__76 T_Dec_20
v4 T_Dec_20
v5
du__'215''45'dec__76 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'215''45'dec__76 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'215''45'dec__76 T_Dec_20
v0 T_Dec_20
v1
  = (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
C__because__32
      ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
         ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
      ((Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du__'215''45'reflects__82
         ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)) ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
         ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
-- Relation.Nullary.Decidable.Core._⊎-dec_
d__'8846''45'dec__86 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8846''45'dec__86 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8846''45'dec__86 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Dec_20
v4 T_Dec_20
v5
  = T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8846''45'dec__86 T_Dec_20
v4 T_Dec_20
v5
du__'8846''45'dec__86 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8846''45'dec__86 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8846''45'dec__86 T_Dec_20
v0 T_Dec_20
v1
  = (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
C__because__32
      ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
         ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
      ((Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du__'8846''45'reflects__98
         ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)) ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
         ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
-- Relation.Nullary.Decidable.Core._→-dec_
d__'8594''45'dec__96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8594''45'dec__96 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8594''45'dec__96 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Dec_20
v4 T_Dec_20
v5
  = T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8594''45'dec__96 T_Dec_20
v4 T_Dec_20
v5
du__'8594''45'dec__96 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8594''45'dec__96 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8594''45'dec__96 T_Dec_20
v0 T_Dec_20
v1
  = (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
C__because__32
      ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
         ((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0)))
         ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
      ((Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du__'8594''45'reflects__114
         ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)) ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
         ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
-- Relation.Nullary.Decidable.Core.dec⇒maybe
d_dec'8658'maybe_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> Maybe AgdaAny
d_dec'8658'maybe_106 :: () -> () -> T_Dec_20 -> Maybe AgdaAny
d_dec'8658'maybe_106 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_106 T_Dec_20
v2
du_dec'8658'maybe_106 :: T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_106 :: T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_106 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                    ((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2))
             else Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      T_Dec_20
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.toSum
d_toSum_110 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_toSum_110 :: () -> () -> T_Dec_20 -> T__'8846'__30
d_toSum_110 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> T__'8846'__30
du_toSum_110 T_Dec_20
v2
du_toSum_110 ::
  T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_toSum_110 :: T_Dec_20 -> T__'8846'__30
du_toSum_110 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                    ((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2))
             else (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                    ((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2))
      T_Dec_20
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.fromSum
d_fromSum_116 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
d_fromSum_116 :: () -> () -> T__'8846'__30 -> T_Dec_20
d_fromSum_116 ~()
v0 ~()
v1 T__'8846'__30
v2 = T__'8846'__30 -> T_Dec_20
du_fromSum_116 T__'8846'__30
v2
du_fromSum_116 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
du_fromSum_116 :: T__'8846'__30 -> T_Dec_20
du_fromSum_116 T__'8846'__30
v0
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
             Bool -> T_Reflects_16 -> T_Dec_20
C__because__32 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
             Bool -> T_Reflects_16 -> T_Dec_20
C__because__32 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
      T__'8846'__30
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.isYes
d_isYes_122 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_isYes_122 :: () -> () -> T_Dec_20 -> Bool
d_isYes_122 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Bool
du_isYes_122 T_Dec_20
v2
du_isYes_122 :: T_Dec_20 -> Bool
du_isYes_122 :: T_Dec_20 -> Bool
du_isYes_122 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2 -> Bool -> Bool
forall a b. a -> b
coe Bool
v1
      T_Dec_20
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.isNo
d_isNo_124 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_isNo_124 :: () -> () -> T_Dec_20 -> Bool
d_isNo_124 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Bool
du_isNo_124 T_Dec_20
v2
du_isNo_124 :: T_Dec_20 -> Bool
du_isNo_124 :: T_Dec_20 -> Bool
du_isNo_124 T_Dec_20
v0
  = (Bool -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
      Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
du_isYes_122 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
-- Relation.Nullary.Decidable.Core.True
d_True_126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_True_126 :: () -> () -> T_Dec_20 -> ()
d_True_126 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
-- Relation.Nullary.Decidable.Core.False
d_False_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_False_128 :: () -> () -> T_Dec_20 -> ()
d_False_128 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
-- Relation.Nullary.Decidable.Core.⌊_⌋
d_'8970'_'8971'_130 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_'8970'_'8971'_130 :: () -> () -> T_Dec_20 -> Bool
d_'8970'_'8971'_130 ()
v0 ()
v1 T_Dec_20
v2 = (T_Dec_20 -> Bool) -> T_Dec_20 -> Bool
forall a b. a -> b
coe T_Dec_20 -> Bool
du_isYes_122 T_Dec_20
v2
-- Relation.Nullary.Decidable.Core.toWitness
d_toWitness_134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_toWitness_134 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_toWitness_134 ~()
v0 ~()
v1 T_Dec_20
v2 ~AgdaAny
v3 = T_Dec_20 -> AgdaAny
du_toWitness_134 T_Dec_20
v2
du_toWitness_134 :: T_Dec_20 -> AgdaAny
du_toWitness_134 :: T_Dec_20 -> AgdaAny
du_toWitness_134 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2
        -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v1)
             ((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2))
      T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.fromWitness
d_fromWitness_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_fromWitness_140 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_fromWitness_140 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_140 T_Dec_20
v2
du_fromWitness_140 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_140 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_140 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then let v3 :: b
v3 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                  AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
forall a. a
v3))
             else (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
      T_Dec_20
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.toWitnessFalse
d_toWitnessFalse_146 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Dec_20 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_toWitnessFalse_146 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_Irrelevant_20
d_toWitnessFalse_146 = () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Decidable.Core.fromWitnessFalse
d_fromWitnessFalse_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Dec_20 ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
d_fromWitnessFalse_152 :: () -> () -> T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
d_fromWitnessFalse_152 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_fromWitnessFalse_152 T_Dec_20
v2
du_fromWitnessFalse_152 ::
  T_Dec_20 ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
du_fromWitnessFalse_152 :: T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_fromWitnessFalse_152 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
forall a b. a -> b
coe
                    (\ AgdaAny
v3 ->
                       AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny
v3
                         ((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)))
             else (let v3 :: b
v3 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                   AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
forall a. a
v3)))
      T_Dec_20
_ -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.from-yes
d_from'45'yes_158 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> AgdaAny
d_from'45'yes_158 :: () -> () -> T_Dec_20 -> AgdaAny
d_from'45'yes_158 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny
du_from'45'yes_158 T_Dec_20
v2
du_from'45'yes_158 :: T_Dec_20 -> AgdaAny
du_from'45'yes_158 :: T_Dec_20 -> AgdaAny
du_from'45'yes_158 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
             else (AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
                    (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.from-no
d_from'45'no_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> AgdaAny
d_from'45'no_164 :: () -> () -> T_Dec_20 -> AgdaAny
d_from'45'no_164 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny
du_from'45'no_164 T_Dec_20
v2
du_from'45'no_164 :: T_Dec_20 -> AgdaAny
du_from'45'no_164 :: T_Dec_20 -> AgdaAny
du_from'45'no_164 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
                    (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
             else (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
      T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.map′
d_map'8242'_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
d_map'8242'_168 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Dec_20
-> T_Dec_20
d_map'8242'_168 ~()
v0 ~()
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 T_Dec_20
v6
  = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 T_Dec_20
v6
du_map'8242'_168 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_Dec_20
v2
  = (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
C__because__32 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v2))
      (case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v2 of
         C__because__32 Bool
v3 T_Reflects_16
v4
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
                then (Bool -> AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du_of_30
                       ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v2)))
                       ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny
v0
                          ((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v4)))
                else (Bool -> AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du_of_30
                       ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v2)))
                       ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                          (\ AgdaAny
v5 ->
                             (T_Reflects_16 -> AgdaAny) -> T_Reflects_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 T_Reflects_16
v4
                               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v5)))
         T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Nullary.Decidable.Core.decidable-stable
d_decidable'45'stable_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Dec_20 ->
  ((AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
d_decidable'45'stable_188 :: ()
-> ()
-> T_Dec_20
-> ((AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20)
-> AgdaAny
d_decidable'45'stable_188 ~()
v0 ~()
v1 T_Dec_20
v2 ~(AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20
v3
  = T_Dec_20 -> AgdaAny
du_decidable'45'stable_188 T_Dec_20
v2
du_decidable'45'stable_188 :: T_Dec_20 -> AgdaAny
du_decidable'45'stable_188 :: T_Dec_20 -> AgdaAny
du_decidable'45'stable_188 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
             else ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                    AgdaAny
forall a. a
erased
      T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.¬-drop-Dec
d_'172''45'drop'45'Dec_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> T_Dec_20
d_'172''45'drop'45'Dec_198 :: () -> () -> T_Dec_20 -> T_Dec_20
d_'172''45'drop'45'Dec_198 ~()
v0 ~()
v1 T_Dec_20
v2
  = T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_198 T_Dec_20
v2
du_'172''45'drop'45'Dec_198 :: T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_198 :: T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_198 T_Dec_20
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 AgdaAny
forall a. a
erased
      (\ AgdaAny
v1 ->
         ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
           (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44)
      ((T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Dec_20
du_'172''63'_70 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
-- Relation.Nullary.Decidable.Core.¬¬-excluded-middle
d_'172''172''45'excluded'45'middle_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (T_Dec_20 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'172''172''45'excluded'45'middle_202 :: () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
d_'172''172''45'excluded'45'middle_202 = () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Decidable.Core.excluded-middle
d_excluded'45'middle_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (T_Dec_20 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_excluded'45'middle_208 :: () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
d_excluded'45'middle_208 = () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Decidable.Core.decToMaybe
d_decToMaybe_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> Maybe AgdaAny
d_decToMaybe_210 :: () -> () -> T_Dec_20 -> Maybe AgdaAny
d_decToMaybe_210 ()
v0 ()
v1 T_Dec_20
v2 = (T_Dec_20 -> Maybe AgdaAny) -> T_Dec_20 -> Maybe AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_106 T_Dec_20
v2
-- Relation.Nullary.Decidable.Core.fromDec
d_fromDec_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_fromDec_212 :: () -> () -> T_Dec_20 -> T__'8846'__30
d_fromDec_212 ()
v0 ()
v1 T_Dec_20
v2 = (T_Dec_20 -> T__'8846'__30) -> T_Dec_20 -> T__'8846'__30
forall a b. a -> b
coe T_Dec_20 -> T__'8846'__30
du_toSum_110 T_Dec_20
v2
-- Relation.Nullary.Decidable.Core.toDec
d_toDec_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
d_toDec_214 :: () -> () -> T__'8846'__30 -> T_Dec_20
d_toDec_214 ()
v0 ()
v1 T__'8846'__30
v2 = (T__'8846'__30 -> T_Dec_20) -> T__'8846'__30 -> T_Dec_20
forall a b. a -> b
coe T__'8846'__30 -> T_Dec_20
du_fromSum_116 T__'8846'__30
v2