{-# 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.Irrelevant
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- 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.Irrelevant.T_Irrelevant_20) ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_dmap_12 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny -> T_Irrelevant_20)
-> T_Dec_20
-> T_Dec_20
d_dmap_12 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~(AgdaAny -> T_Irrelevant_20) -> AgdaAny -> T_Irrelevant_20
v5 T_Dec_20
v6 = (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_dmap_12 AgdaAny -> AgdaAny
v4 T_Dec_20
v6
du_dmap_12 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dmap_12 :: (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_dmap_12 AgdaAny -> AgdaAny
v0 T_Dec_20
v1
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v2 T_Reflects_16
v3
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
             then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v3 of
                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v4
                      -> (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
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                           (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
                           ((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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4))
                    T_Reflects_16
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v3)
                    ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
                       (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
      T_Dec_20
_ -> T_Dec_20
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.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
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_20
-> T_Dec_20
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_20 -> T_Dec_20
du_dcong_40
du_dcong_40 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dcong_40 :: T_Dec_20 -> T_Dec_20
du_dcong_40 = ((AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
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.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
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_20
-> T_Dec_20
-> T_Dec_20
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_20
v12 T_Dec_20
v13
  = T_Dec_20 -> T_Dec_20 -> T_Dec_20
du_dcong'8322'_70 T_Dec_20
v12 T_Dec_20
v13
du_dcong'8322'_70 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dcong'8322'_70 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du_dcong'8322'_70 T_Dec_20
v0 T_Dec_20
v1
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v2 T_Reflects_16
v3
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
             then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v3)
                    (case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 of
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
                         -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
                              then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                                     MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v6
                                       -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                            (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
                                            ((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
forall a. a
erased)
                                     T_Reflects_16
_ -> (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_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
                                               ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                  Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.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)))
                              else (case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                                      T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26
                                        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                             Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
                                             (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
                                                T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
                                      T_Reflects_16
_ -> (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_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
                                                ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                   (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
                                                   (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
                                                      T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))))
                       T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v3)
                    ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
                       (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
      T_Dec_20
_ -> T_Dec_20
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.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
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_20
-> (AgdaAny -> T_Dec_20)
-> T_Dec_20
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_20
v12
             AgdaAny -> T_Dec_20
v13
  = AgdaAny -> T_Dec_20 -> (AgdaAny -> T_Dec_20) -> T_Dec_20
du_dhcong_120 AgdaAny
v9 T_Dec_20
v12 AgdaAny -> T_Dec_20
v13
du_dhcong_120 ::
  AgdaAny ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dhcong_120 :: AgdaAny -> T_Dec_20 -> (AgdaAny -> T_Dec_20) -> T_Dec_20
du_dhcong_120 AgdaAny
v0 T_Dec_20
v1 AgdaAny -> T_Dec_20
v2
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v3 T_Reflects_16
v4
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
             then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v4) ((T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Dec_20
du_dcong_40 ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v2 AgdaAny
v0))
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v4)
                    ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v3)
                       (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
      T_Dec_20
_ -> T_Dec_20
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.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
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_20
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T_Dec_20
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_20
v15 AgdaAny -> T_Dec_20
v16 AgdaAny -> T_Dec_20
v17
  = AgdaAny
-> AgdaAny
-> T_Dec_20
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T_Dec_20
du_dhcong'8322'_180 AgdaAny
v10 AgdaAny
v12 T_Dec_20
v15 AgdaAny -> T_Dec_20
v16 AgdaAny -> T_Dec_20
v17
du_dhcong'8322'_180 ::
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dhcong'8322'_180 :: AgdaAny
-> AgdaAny
-> T_Dec_20
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T_Dec_20
du_dhcong'8322'_180 AgdaAny
v0 AgdaAny
v1 T_Dec_20
v2 AgdaAny -> T_Dec_20
v3 AgdaAny -> T_Dec_20
v4
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v2 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
             then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6) ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Dec_20 -> T_Dec_20
du_dcong'8322'_70 ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v3 AgdaAny
v0) ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v4 AgdaAny
v1))
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6)
                    ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v5)
                       (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
      T_Dec_20
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError