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.Data.List.Relation.Unary.AllPairs where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Bool qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.List qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.List.Relation.Unary.All qualified
  import MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core qualified
  import MAlonzo.Code.Data.Product.Base qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
  import MAlonzo.Code.Relation.Nullary.Reflects qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Data.List.Relation.Unary.AllPairs.head
  d_head_22 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
  d_head_22 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_head_22 v6
  du_head_22 ::
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
  du_head_22 v0
    = case coe v0 of
        MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28 v3 v4
          -> coe v3
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Unary.AllPairs.tail
  d_tail_32 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  d_tail_32 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_tail_32 v6
  du_tail_32 ::
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  du_tail_32 v0
    = case coe v0 of
        MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28 v3 v4
          -> coe v4
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Unary.AllPairs.uncons
  d_uncons_42 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    AgdaAny ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_uncons_42 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 = du_uncons_42
  du_uncons_42 ::
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_uncons_42
    = coe
        MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112
        (coe du_head_22) (coe du_tail_32)
  -- Data.List.Relation.Unary.AllPairs._.map
  d_map_52 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  d_map_52 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 = du_map_52 v6 v7 v8
  du_map_52 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  du_map_52 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C_'91''93'_22
          -> coe v2
        MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28 v5 v6
          -> case coe v1 of
               (:) v7 v8
                 -> coe
                      MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28
                      (coe
                         MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164 (coe v0 v7)
                         (coe v8) (coe v5))
                      (coe du_map_52 (coe v0) (coe v8) (coe v6))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Unary.AllPairs._.zipWith
  d_zipWith_74 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  d_zipWith_74 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10
    = du_zipWith_74 v8 v9 v10
  du_zipWith_74 ::
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  du_zipWith_74 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
          -> case coe v3 of
               MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C_'91''93'_22
                 -> coe seq (coe v4) (coe v3)
               MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28 v7 v8
                 -> case coe v1 of
                      (:) v9 v10
                        -> case coe v4 of
                             MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28 v13 v14
                               -> coe
                                    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28
                                    (coe
                                       MAlonzo.Code.Data.List.Relation.Unary.All.du_zipWith_174
                                       (coe v0 v9) (coe v10)
                                       (coe
                                          MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v7)
                                          (coe v13)))
                                    (coe
                                       du_zipWith_74 (coe v0) (coe v10)
                                       (coe
                                          MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v8)
                                          (coe v14)))
                             _ -> MAlonzo.RTE.mazUnreachableError
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Unary.AllPairs._.unzipWith
  d_unzipWith_88 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    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.Sigma.T_Σ_14) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_unzipWith_88 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10
    = du_unzipWith_88 v8 v9 v10
  du_unzipWith_88 ::
    (AgdaAny ->
     AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_unzipWith_88 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C_'91''93'_22
          -> coe
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v2) (coe v2)
        MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28 v5 v6
          -> case coe v1 of
               (:) v7 v8
                 -> coe
                      MAlonzo.Code.Data.Product.Base.du_zip_198
                      (coe
                         MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28)
                      (coe
                         (\ v9 v10 ->
                            coe
                              MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28))
                      (coe
                         MAlonzo.Code.Data.List.Relation.Unary.All.du_unzipWith_188
                         (coe v0 v7) (coe v8) (coe v5))
                      (coe du_unzipWith_88 (coe v0) (coe v8) (coe v6))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Unary.AllPairs._.zip
  d_zip_106 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  d_zip_106 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_zip_106 v6
  du_zip_106 ::
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  du_zip_106 v0 = coe du_zipWith_74 (coe (\ v1 v2 v3 -> v3)) (coe v0)
  -- Data.List.Relation.Unary.AllPairs._.unzip
  d_unzip_108 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_unzip_108 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_unzip_108 v6
  du_unzip_108 ::
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_unzip_108 v0
    = coe du_unzipWith_88 (coe (\ v1 v2 v3 -> v3)) (coe v0)
  -- Data.List.Relation.Unary.AllPairs.allPairs?
  d_allPairs'63'_110 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_allPairs'63'_110 ~v0 ~v1 ~v2 ~v3 v4 v5
    = du_allPairs'63'_110 v4 v5
  du_allPairs'63'_110 ::
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_allPairs'63'_110 v0 v1
    = case coe v1 of
        []
          -> coe
               MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
               (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
               (coe
                  MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                  (coe
                     MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C_'91''93'_22))
        (:) v2 v3
          -> coe
               MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
               (coe
                  MAlonzo.Code.Data.Product.Base.du_uncurry_244
                  (coe
                     MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28))
               (coe du_uncons_42)
               (coe
                  MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                  (coe
                     MAlonzo.Code.Data.List.Relation.Unary.All.du_all'63'_506
                     (coe v0 v2) (coe v3))
                  (coe du_allPairs'63'_110 (coe v0) (coe v3)))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Unary.AllPairs.irrelevant
  d_irrelevant_120 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_irrelevant_120 = erased
  -- Data.List.Relation.Unary.AllPairs.satisfiable
  d_satisfiable_134 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_satisfiable_134 ~v0 ~v1 ~v2 ~v3 = du_satisfiable_134
  du_satisfiable_134 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_satisfiable_134
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
        (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
        (coe
           MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C_'91''93'_22)
  