content: {-# 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 ~v0 ~v1 ~v2 ~v3 v4 ~v5 v6 = du_dmap_12 v4 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 v0 v1
    = case coe v1 of
        MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v2 v3
          -> if coe v2
               then case coe v3 of
                      MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v4
                        -> coe
                             MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                             (coe v2)
                             (coe
                                MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (coe v0 v4))
                      _ -> MAlonzo.RTE.mazUnreachableError
               else coe
                      seq (coe v3)
                      (coe
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                         (coe v2)
                         (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
        _ -> 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 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 = 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 = coe du_dmap_12 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 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10 ~v11
                   v12 v13
    = du_dcong'8322'_70 v12 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 v0 v1
    = case coe v0 of
        MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v2 v3
          -> if coe v2
               then coe
                      seq (coe v3)
                      (case coe v1 of
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v4 v5
                           -> if coe v4
                                then case coe v5 of
                                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v6
                                         -> coe
                                              MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                              (coe v4)
                                              (coe
                                                 MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                                                 erased)
                                       _ -> coe
                                              seq (coe v4)
                                              (coe
                                                 seq (coe v5)
                                                 (coe
                                                    MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                    (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                                                    (coe
                                                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)))
                                else (case coe v5 of
                                        MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26
                                          -> coe
                                               MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                               (coe v4)
                                               (coe
                                                  MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
                                        _ -> coe
                                               seq (coe v4)
                                               (coe
                                                  seq (coe v5)
                                                  (coe
                                                     MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                     (coe v4)
                                                     (coe
                                                        MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))))
                         _ -> MAlonzo.RTE.mazUnreachableError)
               else coe
                      seq (coe v3)
                      (coe
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                         (coe v2)
                         (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
        _ -> 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 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9 ~v10 ~v11 v12
               v13
    = du_dhcong_120 v9 v12 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 v0 v1 v2
    = case coe v1 of
        MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v3 v4
          -> if coe v3
               then coe seq (coe v4) (coe du_dcong_40 (coe v2 v0))
               else coe
                      seq (coe v4)
                      (coe
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                         (coe v3)
                         (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
        _ -> 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 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10 ~v11
                     v12 ~v13 ~v14 v15 v16 v17
    = du_dhcong'8322'_180 v10 v12 v15 v16 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 v0 v1 v2 v3 v4
    = case coe v2 of
        MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v5 v6
          -> if coe v5
               then coe
                      seq (coe v6) (coe du_dcong'8322'_70 (coe v3 v0) (coe v4 v1))
               else coe
                      seq (coe v6)
                      (coe
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                         (coe v5)
                         (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
        _ -> MAlonzo.RTE.mazUnreachableError
  