{-# 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.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.Bool.Base
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Level
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Relation.Nullary.Decidable.Core.isYes
d_isYes_16 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> Bool
d_isYes_16 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Bool
d_isYes_16 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 = T_Dec_32 -> Bool
du_isYes_16 T_Dec_32
v2
du_isYes_16 :: MAlonzo.Code.Relation.Nullary.T_Dec_32 -> Bool
du_isYes_16 :: T_Dec_32 -> Bool
du_isYes_16 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2 -> Bool -> Bool
forall a b. a -> b
coe Bool
v1
      T_Dec_32
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.isYes≗does
d_isYes'8791'does_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_isYes'8791'does_20 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> T__'8801'__12
d_isYes'8791'does_20 = T_Level_18 -> T_Level_18 -> T_Dec_32 -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.Core.⌊_⌋
d_'8970'_'8971'_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> Bool
d_'8970'_'8971'_22 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Bool
d_'8970'_'8971'_22 T_Level_18
v0 T_Level_18
v1 T_Dec_32
v2 = (T_Dec_32 -> Bool) -> T_Dec_32 -> Bool
forall a b. a -> b
coe T_Dec_32 -> Bool
du_isYes_16 T_Dec_32
v2
-- Relation.Nullary.Decidable.Core.isNo
d_isNo_24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> Bool
d_isNo_24 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Bool
d_isNo_24 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 = T_Dec_32 -> Bool
du_isNo_24 T_Dec_32
v2
du_isNo_24 :: MAlonzo.Code.Relation.Nullary.T_Dec_32 -> Bool
du_isNo_24 :: T_Dec_32 -> Bool
du_isNo_24 T_Dec_32
v0
  = (Bool -> Bool) -> Any -> Bool
forall a b. a -> b
coe
      Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22 ((T_Dec_32 -> Bool) -> Any -> Any
forall a b. a -> b
coe T_Dec_32 -> Bool
du_isYes_16 (T_Dec_32 -> Any
forall a b. a -> b
coe T_Dec_32
v0))
-- Relation.Nullary.Decidable.Core.True
d_True_26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> ()
d_True_26 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Level_18
d_True_26 = T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Level_18
forall a. a
erased
-- Relation.Nullary.Decidable.Core.False
d_False_30 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> ()
d_False_30 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Level_18
d_False_30 = T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Level_18
forall a. a
erased
-- Relation.Nullary.Decidable.Core.toWitness
d_toWitness_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> AgdaAny -> AgdaAny
d_toWitness_36 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any -> Any
d_toWitness_36 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 ~Any
v3 = T_Dec_32 -> Any
du_toWitness_36 T_Dec_32
v2
du_toWitness_36 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 -> AgdaAny
du_toWitness_36 :: T_Dec_32 -> Any
du_toWitness_36 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2
        -> (Any -> Any -> Any) -> Any -> Any -> Any
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)
             ((T_Reflects_14 -> Any) -> Any -> Any
forall a b. a -> b
coe T_Reflects_14 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v2))
      T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.fromWitness
d_fromWitness_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> AgdaAny -> AgdaAny
d_fromWitness_42 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any -> Any
d_fromWitness_42 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 = T_Dec_32 -> Any -> Any
du_fromWitness_42 T_Dec_32
v2
du_fromWitness_42 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 -> AgdaAny -> AgdaAny
du_fromWitness_42 :: T_Dec_32 -> Any -> Any
du_fromWitness_42 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then let v3 :: b
v3 = T_Level_18 -> b
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                  Any -> Any -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v4 -> Any
forall a. a
v3))
             else (T_Reflects_14 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Reflects_14 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v2)
      T_Dec_32
_ -> Any -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.toWitnessFalse
d_toWitnessFalse_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_toWitnessFalse_48 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any -> Any -> T_'8869'_4
d_toWitnessFalse_48 = T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any -> Any -> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Decidable.Core.fromWitnessFalse
d_fromWitnessFalse_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) -> AgdaAny
d_fromWitnessFalse_54 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> (Any -> T_'8869'_4) -> Any
d_fromWitnessFalse_54 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 = T_Dec_32 -> (Any -> T_'8869'_4) -> Any
du_fromWitnessFalse_54 T_Dec_32
v2
du_fromWitnessFalse_54 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) -> AgdaAny
du_fromWitnessFalse_54 :: T_Dec_32 -> (Any -> T_'8869'_4) -> Any
du_fromWitnessFalse_54 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (Any -> Any) -> (Any -> T_'8869'_4) -> Any
forall a b. a -> b
coe
                    (\ Any
v3 ->
                       Any -> Any -> Any
forall a b. a -> b
coe
                         Any
v3
                         ((T_Reflects_14 -> Any) -> Any -> Any
forall a b. a -> b
coe T_Reflects_14 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v2)))
             else (let v3 :: b
v3 = T_Level_18 -> b
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                   Any -> (Any -> T_'8869'_4) -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v4 -> Any
forall a. a
v3)))
      T_Dec_32
_ -> (Any -> T_'8869'_4) -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core._.From-yes
d_From'45'yes_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> ()
d_From'45'yes_66 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Level_18
d_From'45'yes_66 = T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Level_18
forall a. a
erased
-- Relation.Nullary.Decidable.Core._.from-yes
d_from'45'yes_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> AgdaAny
d_from'45'yes_70 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any
d_from'45'yes_70 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 = T_Dec_32 -> Any
du_from'45'yes_70 T_Dec_32
v2
du_from'45'yes_70 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 -> AgdaAny
du_from'45'yes_70 :: T_Dec_32 -> Any
du_from'45'yes_70 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (T_Reflects_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
                    T_Reflects_14 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v2)
             else (Any -> T_Lift_8) -> Any -> Any
forall a b. a -> b
coe
                    Any -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
                    (T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core._.From-no
d_From'45'no_74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> ()
d_From'45'no_74 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Level_18
d_From'45'no_74 = T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Level_18
forall a. a
erased
-- Relation.Nullary.Decidable.Core._.from-no
d_from'45'no_78 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> AgdaAny
d_from'45'no_78 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any
d_from'45'no_78 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 = T_Dec_32 -> Any
du_from'45'no_78 T_Dec_32
v2
du_from'45'no_78 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 -> AgdaAny
du_from'45'no_78 :: T_Dec_32 -> Any
du_from'45'no_78 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then (Any -> T_Lift_8) -> Any -> Any
forall a b. a -> b
coe
                    Any -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
                    (T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
             else (T_Reflects_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
                    T_Reflects_14 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v2)
      T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.dec-true
d_dec'45'true_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'true_84 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any -> T__'8801'__12
d_dec'45'true_84 = T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.Core.dec-false
d_dec'45'false_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'false_94 :: T_Level_18
-> T_Level_18 -> T_Dec_32 -> (Any -> T_'8869'_4) -> T__'8801'__12
d_dec'45'false_94 = T_Level_18
-> T_Level_18 -> T_Dec_32 -> (Any -> T_'8869'_4) -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.Core.dec-yes
d_dec'45'yes_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_dec'45'yes_106 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> Any -> T_Σ_14
d_dec'45'yes_106 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 ~Any
v3 = T_Dec_32 -> T_Σ_14
du_dec'45'yes_106 T_Dec_32
v2
du_dec'45'yes_106 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_dec'45'yes_106 :: T_Dec_32 -> T_Σ_14
du_dec'45'yes_106 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
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_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v2 of
                MAlonzo.Code.Relation.Nullary.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_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
      T_Dec_32
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.dec-no
d_dec'45'no_124 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_dec'45'no_124 :: T_Level_18
-> T_Level_18 -> T_Dec_32 -> (Any -> T_'8869'_4) -> T_Σ_14
d_dec'45'no_124 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 ~Any -> T_'8869'_4
v3 = T_Dec_32 -> T_Σ_14
du_dec'45'no_124 T_Dec_32
v2
du_dec'45'no_124 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_dec'45'no_124 :: T_Dec_32 -> T_Σ_14
du_dec'45'no_124 T_Dec_32
v0
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
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)
             ((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v2)
                ((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
forall a. a
erased Any
forall a. a
erased))
      T_Dec_32
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Decidable.Core.dec-yes-irr
d_dec'45'yes'45'irr_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (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_142 :: T_Level_18
-> T_Level_18
-> T_Dec_32
-> (Any -> Any -> T__'8801'__12)
-> Any
-> T__'8801'__12
d_dec'45'yes'45'irr_142 = T_Level_18
-> T_Level_18
-> T_Dec_32
-> (Any -> Any -> T__'8801'__12)
-> Any
-> T__'8801'__12
forall a. a
erased
-- 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) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_map'8242'_168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> (Any -> Any)
-> T_Dec_32
-> T_Dec_32
d_map'8242'_168 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 Any -> Any
v4 ~Any -> Any
v5 T_Dec_32
v6 = (Any -> Any) -> T_Dec_32 -> T_Dec_32
du_map'8242'_168 Any -> Any
v4 T_Dec_32
v6
du_map'8242'_168 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_map'8242'_168 :: (Any -> Any) -> T_Dec_32 -> T_Dec_32
du_map'8242'_168 Any -> Any
v0 T_Dec_32
v1
  = (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
      Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
      ((T_Dec_32 -> Bool) -> Any -> Any
forall a b. a -> b
coe T_Dec_32 -> Bool
MAlonzo.Code.Relation.Nullary.d_does_42 (T_Dec_32 -> Any
forall a b. a -> b
coe T_Dec_32
v1))
      (case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v1 of
         MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v2 T_Reflects_14
v3
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
                then (Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
                       Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
                       ((Any -> Any) -> Any -> Any
forall a b. a -> b
coe
                          Any -> Any
v0
                          ((T_Reflects_14 -> Any) -> Any -> Any
forall a b. a -> b
coe T_Reflects_14 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v3)))
                else T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
         T_Dec_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)