{-# 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.recompute-irrelevant-id
d_recompute'45'irrelevant'45'id_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_recompute'45'irrelevant'45'id_68 :: ()
-> ()
-> T_Dec_20
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> AgdaAny
-> T__'8801'__12
d_recompute'45'irrelevant'45'id_68 = ()
-> ()
-> T_Dec_20
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.Core.T?
d_T'63'_72 :: Bool -> T_Dec_20
d_T'63'_72 :: Bool -> T_Dec_20
d_T'63'_72 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_70 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
-- Relation.Nullary.Decidable.Core.¬?
d_'172''63'_76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> T_Dec_20
d_'172''63'_76 :: () -> () -> T_Dec_20 -> T_Dec_20
d_'172''63'_76 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> T_Dec_20
du_'172''63'_76 T_Dec_20
v2
du_'172''63'_76 :: T_Dec_20 -> T_Dec_20
du_'172''63'_76 :: T_Dec_20 -> T_Dec_20
du_'172''63'_76 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_74
         ((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_'8868''45'dec_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> T_Dec_20
d_'8868''45'dec_82 :: () -> T_Dec_20
d_'8868''45'dec_82 ~()
v0 = T_Dec_20
du_'8868''45'dec_82
du_'8868''45'dec_82 :: T_Dec_20
du_'8868''45'dec_82 :: T_Dec_20
du_'8868''45'dec_82
  = (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)
      (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
         T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du_'8868''45'reflects_66)
-- Relation.Nullary.Decidable.Core._×-dec_
d__'215''45'dec__84 ::
  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__84 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'215''45'dec__84 ~()
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__84 T_Dec_20
v4 T_Dec_20
v5
du__'215''45'dec__84 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'215''45'dec__84 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'215''45'dec__84 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__86
         ((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_'8869''45'dec_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> T_Dec_20
d_'8869''45'dec_94 :: () -> T_Dec_20
d_'8869''45'dec_94 ~()
v0 = T_Dec_20
du_'8869''45'dec_94
du_'8869''45'dec_94 :: T_Dec_20
du_'8869''45'dec_94 :: T_Dec_20
du_'8869''45'dec_94
  = (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.du_'8869''45'reflects_64)
-- Relation.Nullary.Decidable.Core._⊎-dec_
d__'8846''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__'8846''45'dec__96 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8846''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__'8846''45'dec__96 T_Dec_20
v4 T_Dec_20
v5
du__'8846''45'dec__96 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8846''45'dec__96 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8846''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 ((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__102
         ((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__106 ::
  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__106 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8594''45'dec__106 ~()
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__106 T_Dec_20
v4 T_Dec_20
v5
du__'8594''45'dec__106 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8594''45'dec__106 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8594''45'dec__106 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__118
         ((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_116 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> Maybe AgdaAny
d_dec'8658'maybe_116 :: () -> () -> T_Dec_20 -> Maybe AgdaAny
d_dec'8658'maybe_116 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_116 T_Dec_20
v2
du_dec'8658'maybe_116 :: T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_116 :: T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_116 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_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_toSum_120 :: () -> () -> T_Dec_20 -> T__'8846'__30
d_toSum_120 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> T__'8846'__30
du_toSum_120 T_Dec_20
v2
du_toSum_120 ::
  T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_toSum_120 :: T_Dec_20 -> T__'8846'__30
du_toSum_120 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_126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
d_fromSum_126 :: () -> () -> T__'8846'__30 -> T_Dec_20
d_fromSum_126 ~()
v0 ~()
v1 T__'8846'__30
v2 = T__'8846'__30 -> T_Dec_20
du_fromSum_126 T__'8846'__30
v2
du_fromSum_126 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
du_fromSum_126 :: T__'8846'__30 -> T_Dec_20
du_fromSum_126 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_132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_isYes_132 :: () -> () -> T_Dec_20 -> Bool
d_isYes_132 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Bool
du_isYes_132 T_Dec_20
v2
du_isYes_132 :: T_Dec_20 -> Bool
du_isYes_132 :: T_Dec_20 -> Bool
du_isYes_132 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_134 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_isNo_134 :: () -> () -> T_Dec_20 -> Bool
d_isNo_134 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Bool
du_isNo_134 T_Dec_20
v2
du_isNo_134 :: T_Dec_20 -> Bool
du_isNo_134 :: T_Dec_20 -> Bool
du_isNo_134 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_132 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
-- Relation.Nullary.Decidable.Core.True
d_True_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_True_136 :: () -> () -> T_Dec_20 -> ()
d_True_136 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
-- Relation.Nullary.Decidable.Core.False
d_False_138 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_False_138 :: () -> () -> T_Dec_20 -> ()
d_False_138 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
-- Relation.Nullary.Decidable.Core.⌊_⌋
d_'8970'_'8971'_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_'8970'_'8971'_140 :: () -> () -> T_Dec_20 -> Bool
d_'8970'_'8971'_140 ()
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_132 T_Dec_20
v2
-- Relation.Nullary.Decidable.Core.toWitness
d_toWitness_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_toWitness_144 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_toWitness_144 ~()
v0 ~()
v1 T_Dec_20
v2 ~AgdaAny
v3 = T_Dec_20 -> AgdaAny
du_toWitness_144 T_Dec_20
v2
du_toWitness_144 :: T_Dec_20 -> AgdaAny
du_toWitness_144 :: T_Dec_20 -> AgdaAny
du_toWitness_144 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_150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_fromWitness_150 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_fromWitness_150 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_150 T_Dec_20
v2
du_fromWitness_150 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_150 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_150 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_156 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Dec_20 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_toWitnessFalse_156 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_Irrelevant_20
d_toWitnessFalse_156 = () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Decidable.Core.fromWitnessFalse
d_fromWitnessFalse_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  T_Dec_20 ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
d_fromWitnessFalse_162 :: () -> () -> T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
d_fromWitnessFalse_162 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_fromWitnessFalse_162 T_Dec_20
v2
du_fromWitnessFalse_162 ::
  T_Dec_20 ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
du_fromWitnessFalse_162 :: T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_fromWitnessFalse_162 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_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> AgdaAny
d_from'45'yes_168 :: () -> () -> T_Dec_20 -> AgdaAny
d_from'45'yes_168 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny
du_from'45'yes_168 T_Dec_20
v2
du_from'45'yes_168 :: T_Dec_20 -> AgdaAny
du_from'45'yes_168 :: T_Dec_20 -> AgdaAny
du_from'45'yes_168 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_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> AgdaAny
d_from'45'no_174 :: () -> () -> T_Dec_20 -> AgdaAny
d_from'45'no_174 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny
du_from'45'no_174 T_Dec_20
v2
du_from'45'no_174 :: T_Dec_20 -> AgdaAny
du_from'45'no_174 :: T_Dec_20 -> AgdaAny
du_from'45'no_174 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'_178 ::
  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'_178 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Dec_20
-> T_Dec_20
d_map'8242'_178 ~()
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'_178 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 T_Dec_20
v6
du_map'8242'_178 ::
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_178 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_178 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'_178 ((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'_178 ((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_198 ::
  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_198 :: ()
-> ()
-> T_Dec_20
-> ((AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20)
-> AgdaAny
d_decidable'45'stable_198 ~()
v0 ~()
v1 T_Dec_20
v2 ~(AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20
v3
  = T_Dec_20 -> AgdaAny
du_decidable'45'stable_198 T_Dec_20
v2
du_decidable'45'stable_198 :: T_Dec_20 -> AgdaAny
du_decidable'45'stable_198 :: T_Dec_20 -> AgdaAny
du_decidable'45'stable_198 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_208 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> T_Dec_20
d_'172''45'drop'45'Dec_208 :: () -> () -> T_Dec_20 -> T_Dec_20
d_'172''45'drop'45'Dec_208 ~()
v0 ~()
v1 T_Dec_20
v2
  = T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_208 T_Dec_20
v2
du_'172''45'drop'45'Dec_208 :: T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_208 :: T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_208 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'_178 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'_76 (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_212 ::
  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_212 :: () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
d_'172''172''45'excluded'45'middle_212 = () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Decidable.Core.excluded-middle
d_excluded'45'middle_218 ::
  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_218 :: () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
d_excluded'45'middle_218 = () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Decidable.Core.decToMaybe
d_decToMaybe_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> Maybe AgdaAny
d_decToMaybe_220 :: () -> () -> T_Dec_20 -> Maybe AgdaAny
d_decToMaybe_220 ()
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_116 T_Dec_20
v2
-- Relation.Nullary.Decidable.Core.fromDec
d_fromDec_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_fromDec_222 :: () -> () -> T_Dec_20 -> T__'8846'__30
d_fromDec_222 ()
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_120 T_Dec_20
v2
-- Relation.Nullary.Decidable.Core.toDec
d_toDec_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
d_toDec_224 :: () -> () -> T__'8846'__30 -> T_Dec_20
d_toDec_224 ()
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_126 T__'8846'__30
v2