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.Reflection.AST.Argument where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.Reflection qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.List.Base qualified
  import MAlonzo.Code.Data.Product.Base qualified
  import MAlonzo.Code.Reflection.AST.Argument.Information qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.Core 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
  
  -- Reflection.AST.Argument.Args
  d_Args_38 :: MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
  d_Args_38 = erased
  -- Reflection.AST.Argument.map
  d_map_54 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88
  d_map_54 ~v0 ~v1 ~v2 ~v3 v4 v5 = du_map_54 v4 v5
  du_map_54 ::
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88
  du_map_54 v0 v1
    = case coe v1 of
        MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 v2 v3
          -> coe
               MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 (coe v2) (coe v0 v3)
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Reflection.AST.Argument.map-Args
  d_map'45'Args_62 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
    [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88]
  d_map'45'Args_62 ~v0 ~v1 ~v2 ~v3 v4 v5 = du_map'45'Args_62 v4 v5
  du_map'45'Args_62 ::
    (AgdaAny -> AgdaAny) ->
    [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
    [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88]
  du_map'45'Args_62 v0 v1
    = coe
        MAlonzo.Code.Data.List.Base.du_map_22 (coe du_map_54 (coe v0))
        (coe v1)
  -- Reflection.AST.Argument.arg-injective₁
  d_arg'45'injective'8321'_68 ::
    MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_arg'45'injective'8321'_68 = erased
  -- Reflection.AST.Argument.arg-injective₂
  d_arg'45'injective'8322'_70 ::
    MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_arg'45'injective'8322'_70 = erased
  -- Reflection.AST.Argument.arg-injective
  d_arg'45'injective_72 ::
    MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_arg'45'injective_72 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
    = du_arg'45'injective_72
  du_arg'45'injective_72 ::
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_arg'45'injective_72
    = coe
        MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 erased erased
  -- Reflection.AST.Argument.unArg
  d_unArg_74 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 -> AgdaAny
  d_unArg_74 ~v0 ~v1 v2 = du_unArg_74 v2
  du_unArg_74 ::
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 -> AgdaAny
  du_unArg_74 v0
    = case coe v0 of
        MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 v1 v2 -> coe v2
        _                                                   -> MAlonzo.RTE.mazUnreachableError
  -- Reflection.AST.Argument.unArg-dec
  d_unArg'45'dec_84 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_unArg'45'dec_84 ~v0 ~v1 v2 v3 v4 = du_unArg'45'dec_84 v2 v3 v4
  du_unArg'45'dec_84 ::
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_unArg'45'dec_84 v0 v1 v2
    = case coe v0 of
        MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 v3 v4
          -> case coe v1 of
               MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 v5 v6
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                      (coe MAlonzo.Code.Data.Product.Base.du_uncurry_244 erased)
                      (coe du_arg'45'injective_72)
                      (coe
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                         (coe
                            MAlonzo.Code.Reflection.AST.Argument.Information.d__'8799'__30
                            (coe v3) (coe v5))
                         (coe v2))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Reflection.AST.Argument.≡-dec
  d_'8801''45'dec_96 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_'8801''45'dec_96 ~v0 ~v1 v2 v3 v4 = du_'8801''45'dec_96 v2 v3 v4
  du_'8801''45'dec_96 ::
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_'8801''45'dec_96 v0 v1 v2
    = coe
        du_unArg'45'dec_84 (coe v1) (coe v2)
        (coe v0 (coe du_unArg_74 (coe v1)) (coe du_unArg_74 (coe v2)))
  