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.Product where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive 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.Product.map-Σ
  d_map'45'Σ_48 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_map'45'Σ_48 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10
    = du_map'45'Σ_48 v8 v9 v10
  du_map'45'Σ_48 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_map'45'Σ_48 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
          -> coe
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v0 v3)
               (coe v1 v3 v4)
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.Product.map-Σ′
  d_map'45'Σ'8242'_76 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_map'45'Σ'8242'_76 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10
    = du_map'45'Σ'8242'_76 v8 v9 v10
  du_map'45'Σ'8242'_76 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_map'45'Σ'8242'_76 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
          -> coe
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v0 v3) (coe v1 v4)
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.Product.zipWith
  d_zipWith_122 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
  d_zipWith_122 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10 ~v11
                ~v12 ~v13 v14 v15 v16 v17 v18
    = du_zipWith_122 v14 v15 v16 v17 v18
  du_zipWith_122 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
  du_zipWith_122 v0 v1 v2 v3 v4
    = case coe v3 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v5 v6
          -> case coe v4 of
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v7 v8
                 -> coe v2 (coe v0 v5 v7) (coe v1 v5 v7 v6 v8)
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.Product.∄
  d_'8708'_140 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> ()) -> ()
  d_'8708'_140 = erased
  -- Data.Product.∃!
  d_'8707''33'_146 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> ()
  d_'8707''33'_146 = erased
  -- Data.Product.∄-syntax
  d_'8708''45'syntax_158 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> ()) -> ()
  d_'8708''45'syntax_158 = erased
  