{-# 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.Utils.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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Relation.Nullary

-- Utils.Decidable.dmap
d_dmap_12 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  ((AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
   AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dmap_12 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> ((AgdaAny -> T_'8869'_4) -> AgdaAny -> T_'8869'_4)
-> T_Dec_32
-> T_Dec_32
d_dmap_12 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~(AgdaAny -> T_'8869'_4) -> AgdaAny -> T_'8869'_4
v5 T_Dec_32
v6 = (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
du_dmap_12 AgdaAny -> AgdaAny
v4 T_Dec_32
v6
du_dmap_12 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dmap_12 :: (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
du_dmap_12 AgdaAny -> AgdaAny
v0 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 case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v3 of
                    MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v4
                      -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                           Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
                           ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4))
                    T_Reflects_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v3)
                    ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
                       (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
      T_Dec_32
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Decidable.dcong
d_dcong_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dcong_40 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> (T__'8801'__12 -> T__'8801'__12)
-> T_Dec_32
-> T_Dec_32
d_dcong_40 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~AgdaAny -> AgdaAny
v6 ~T__'8801'__12 -> T__'8801'__12
v7 = T_Dec_32 -> T_Dec_32
du_dcong_40
du_dcong_40 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dcong_40 :: T_Dec_32 -> T_Dec_32
du_dcong_40 = ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
du_dmap_12 AgdaAny
forall a. a
erased
-- Utils.Decidable.dcong₂
d_dcong'8322'_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  () ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dcong'8322'_70 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8801'__12 -> T_Σ_14)
-> T_Dec_32
-> T_Dec_32
-> T_Dec_32
d_dcong'8322'_70 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9 ~AgdaAny -> AgdaAny -> AgdaAny
v10 ~T__'8801'__12 -> T_Σ_14
v11
                 T_Dec_32
v12 T_Dec_32
v13
  = T_Dec_32 -> T_Dec_32 -> T_Dec_32
du_dcong'8322'_70 T_Dec_32
v12 T_Dec_32
v13
du_dcong'8322'_70 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dcong'8322'_70 :: T_Dec_32 -> T_Dec_32 -> T_Dec_32
du_dcong'8322'_70 T_Dec_32
v0 T_Dec_32
v1
  = 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
v2 T_Reflects_14
v3
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
             then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v3)
                    (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
v4 T_Reflects_14
v5
                         -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
                              then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v5 of
                                     MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v6
                                       -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
                                            ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
forall a. a
erased)
                                     T_Reflects_14
_ -> (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
v4)
                                            ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v5)
                                               ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                  Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                                                  (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                                                  (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
                                                     T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)))
                              else (case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v5 of
                                      T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
                                        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
                                             (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
                                      T_Reflects_14
_ -> (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
v4)
                                             ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v5)
                                                ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                                                   (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
                                                   (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
                                                      T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))))
                       T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v3)
                    ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
                       (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
      T_Dec_32
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Decidable.dhcong
d_dhcong_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  () ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dhcong_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8801'__12 -> T_Σ_14)
-> T_Dec_32
-> (AgdaAny -> T_Dec_32)
-> T_Dec_32
d_dhcong_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny
v6 ~AgdaAny
v7 ~AgdaAny
v8 AgdaAny
v9 ~AgdaAny -> AgdaAny -> AgdaAny
v10 ~T__'8801'__12 -> T_Σ_14
v11 T_Dec_32
v12
             AgdaAny -> T_Dec_32
v13
  = AgdaAny -> T_Dec_32 -> (AgdaAny -> T_Dec_32) -> T_Dec_32
du_dhcong_120 AgdaAny
v9 T_Dec_32
v12 AgdaAny -> T_Dec_32
v13
du_dhcong_120 ::
  AgdaAny ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dhcong_120 :: AgdaAny -> T_Dec_32 -> (AgdaAny -> T_Dec_32) -> T_Dec_32
du_dhcong_120 AgdaAny
v0 T_Dec_32
v1 AgdaAny -> T_Dec_32
v2
  = 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
v3 T_Reflects_14
v4
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
             then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v4) ((T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> T_Dec_32
du_dcong_40 ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v2 AgdaAny
v0))
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v4)
                    ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v3)
                       (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
      T_Dec_32
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Decidable.dhcong₂
d_dhcong'8322'_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  () ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dhcong'8322'_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8801'__12 -> T_Σ_14)
-> T_Dec_32
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T_Dec_32
d_dhcong'8322'_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9 AgdaAny
v10 ~AgdaAny
v11
                   AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~T__'8801'__12 -> T_Σ_14
v14 T_Dec_32
v15 AgdaAny -> T_Dec_32
v16 AgdaAny -> T_Dec_32
v17
  = AgdaAny
-> AgdaAny
-> T_Dec_32
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T_Dec_32
du_dhcong'8322'_180 AgdaAny
v10 AgdaAny
v12 T_Dec_32
v15 AgdaAny -> T_Dec_32
v16 AgdaAny -> T_Dec_32
v17
du_dhcong'8322'_180 ::
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dhcong'8322'_180 :: AgdaAny
-> AgdaAny
-> T_Dec_32
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T_Dec_32
du_dhcong'8322'_180 AgdaAny
v0 AgdaAny
v1 T_Dec_32
v2 AgdaAny -> T_Dec_32
v3 AgdaAny -> T_Dec_32
v4
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v2 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v5 T_Reflects_14
v6
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
             then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v6) ((T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> T_Dec_32 -> T_Dec_32
du_dcong'8322'_70 ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v3 AgdaAny
v0) ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v4 AgdaAny
v1))
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v6)
                    ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v5)
                       (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
      T_Dec_32
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError