{-# 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.Function.Nary.NonDependent.Base 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.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Level

-- Function.Nary.NonDependent.Base.Levels
d_Levels_20 :: Integer -> ()
d_Levels_20 :: Integer -> ()
d_Levels_20 = Integer -> ()
forall a. a
erased
-- Function.Nary.NonDependent.Base.⨆
d_'10758'_26 ::
  Integer -> AgdaAny -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'10758'_26 :: Integer -> AgdaAny -> ()
d_'10758'_26 Integer
v0 AgdaAny
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> () -> ()
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Primitive.d_lzero_20
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> ()
forall a b. a -> b
coe
             (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v1 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
                  -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> () -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> ()
forall {p1} {p2}. p1 -> p2 -> ()
MAlonzo.Code.Agda.Primitive.d__'8852'__30 AgdaAny
v3
                       (Integer -> AgdaAny -> ()
d_'10758'_26 (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Function.Nary.NonDependent.Base.Sets
d_Sets_38 :: Integer -> AgdaAny -> ()
d_Sets_38 :: Integer -> AgdaAny -> ()
d_Sets_38 = Integer -> AgdaAny -> ()
forall a. a
erased
-- Function.Nary.NonDependent.Base.Arrows
d_Arrows_52 ::
  Integer ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  AgdaAny -> AgdaAny -> () -> ()
d_Arrows_52 :: Integer -> () -> AgdaAny -> AgdaAny -> () -> ()
d_Arrows_52 = Integer -> () -> AgdaAny -> AgdaAny -> () -> ()
forall a. a
erased
-- Function.Nary.NonDependent.Base._⇉_
d__'8649'__70 ::
  Integer ->
  AgdaAny ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> AgdaAny -> () -> ()
d__'8649'__70 :: Integer -> AgdaAny -> () -> AgdaAny -> () -> ()
d__'8649'__70 = Integer -> AgdaAny -> () -> AgdaAny -> () -> ()
forall a. a
erased
-- Function.Nary.NonDependent.Base._<$>_
d__'60''36''62'__78 ::
  (MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()) ->
  Integer -> AgdaAny -> AgdaAny -> AgdaAny
d__'60''36''62'__78 :: (() -> () -> ()) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny
d__'60''36''62'__78 () -> () -> ()
v0 Integer
v1 AgdaAny
v2 AgdaAny
v3
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
             (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v3 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v5 AgdaAny
v6
                  -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                       ((() -> () -> ()) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> () -> ()
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2)) AgdaAny
v5)
                       (((() -> () -> ()) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          (() -> () -> ()) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny
d__'60''36''62'__78 AgdaAny
forall a. a
erased (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)
                          ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Function.Nary.NonDependent.Base.lmap
d_lmap_94 ::
  (MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18) ->
  Integer -> AgdaAny -> AgdaAny
d_lmap_94 :: (() -> ()) -> Integer -> AgdaAny -> AgdaAny
d_lmap_94 () -> ()
v0 Integer
v1 AgdaAny
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
             (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
                  -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 ((() -> ()) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> ()
v0 AgdaAny
v4)
                       (((() -> ()) -> Integer -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (() -> ()) -> Integer -> AgdaAny -> AgdaAny
d_lmap_94 ((() -> ()) -> AgdaAny
forall a b. a -> b
coe () -> ()
v0) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Function.Nary.NonDependent.Base.smap
d_smap_116 ::
  (MAlonzo.Code.Agda.Primitive.T_Level_18 ->
   MAlonzo.Code.Agda.Primitive.T_Level_18) ->
  (MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()) ->
  Integer -> AgdaAny -> AgdaAny -> AgdaAny
d_smap_116 :: (() -> ())
-> (() -> () -> ()) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny
d_smap_116 ~() -> ()
v0 () -> () -> ()
v1 Integer
v2 AgdaAny
v3 AgdaAny
v4 = (() -> () -> ()) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny
du_smap_116 () -> () -> ()
v1 Integer
v2 AgdaAny
v3 AgdaAny
v4
du_smap_116 ::
  (MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()) ->
  Integer -> AgdaAny -> AgdaAny -> AgdaAny
du_smap_116 :: (() -> () -> ()) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny
du_smap_116 () -> () -> ()
v0 Integer
v1 AgdaAny
v2 AgdaAny
v3
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
             (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v3 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v5 AgdaAny
v6
                  -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                       ((() -> () -> ()) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> () -> ()
v0 (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2)) AgdaAny
v5)
                       (((() -> () -> ()) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          (() -> () -> ()) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny
du_smap_116 AgdaAny
forall a. a
erased (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)
                          ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Function.Nary.NonDependent.Base.mapₙ
d_map'8345'_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_map'8345'_140 :: ()
-> ()
-> ()
-> ()
-> Integer
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_map'8345'_140 ~()
v0 ~()
v1 ~()
v2 ~()
v3 Integer
v4 ~AgdaAny
v5 ~AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8
  = Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map'8345'_140 Integer
v4 AgdaAny -> AgdaAny
v7 AgdaAny
v8
du_map'8345'_140 ::
  Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map'8345'_140 :: Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map'8345'_140 Integer
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2
      Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
                ((Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map'8345'_140 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Function.Nary.NonDependent.Base._%=_⊢_
d__'37''61'_'8866'__158 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'37''61'_'8866'__158 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> Integer
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d__'37''61'_'8866'__158 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 Integer
v6 ~AgdaAny
v7 ~AgdaAny
v8 AgdaAny -> AgdaAny
v9 AgdaAny
v10
  = Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du__'37''61'_'8866'__158 Integer
v6 AgdaAny -> AgdaAny
v9 AgdaAny
v10
du__'37''61'_'8866'__158 ::
  Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du__'37''61'_'8866'__158 :: Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du__'37''61'_'8866'__158 Integer
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map'8345'_140 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v3 ->
            ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
              ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
-- Function.Nary.NonDependent.Base._∷=_⊢_
d__'8759''61'_'8866'__174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d__'8759''61'_'8866'__174 :: ()
-> ()
-> ()
-> ()
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'8759''61'_'8866'__174 ~()
v0 ~()
v1 ~()
v2 ~()
v3 Integer
v4 ~AgdaAny
v5 ~AgdaAny
v6 AgdaAny
v7 AgdaAny
v8
  = Integer -> AgdaAny -> AgdaAny -> AgdaAny
du__'8759''61'_'8866'__174 Integer
v4 AgdaAny
v7 AgdaAny
v8
du__'8759''61'_'8866'__174 ::
  Integer -> AgdaAny -> AgdaAny -> AgdaAny
du__'8759''61'_'8866'__174 :: Integer -> AgdaAny -> AgdaAny -> AgdaAny
du__'8759''61'_'8866'__174 Integer
v0 AgdaAny
v1 AgdaAny
v2
  = (Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map'8345'_140 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 AgdaAny
v1)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
-- Function.Nary.NonDependent.Base.holeₙ
d_hole'8345'_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d_hole'8345'_190 :: ()
-> ()
-> ()
-> ()
-> Integer
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
d_hole'8345'_190 ~()
v0 ~()
v1 ~()
v2 ~()
v3 Integer
v4 ~AgdaAny
v5 ~AgdaAny
v6 AgdaAny -> AgdaAny
v7
  = Integer -> (AgdaAny -> AgdaAny) -> AgdaAny
du_hole'8345'_190 Integer
v4 AgdaAny -> AgdaAny
v7
du_hole'8345'_190 :: Integer -> (AgdaAny -> AgdaAny) -> AgdaAny
du_hole'8345'_190 :: Integer -> (AgdaAny -> AgdaAny) -> AgdaAny
du_hole'8345'_190 Integer
v0 AgdaAny -> AgdaAny
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
                ((Integer -> (AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> (AgdaAny -> AgdaAny) -> AgdaAny
du_hole'8345'_190 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 AgdaAny
v4 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v4 AgdaAny
v3)))
-- Function.Nary.NonDependent.Base.constₙ
d_const'8345'_208 ::
  Integer ->
  AgdaAny ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  AgdaAny -> () -> AgdaAny -> AgdaAny
d_const'8345'_208 :: Integer -> AgdaAny -> () -> AgdaAny -> () -> AgdaAny -> AgdaAny
d_const'8345'_208 Integer
v0 ~AgdaAny
v1 ~()
v2 ~AgdaAny
v3 ~()
v4 AgdaAny
v5 = Integer -> AgdaAny -> AgdaAny
du_const'8345'_208 Integer
v0 AgdaAny
v5
du_const'8345'_208 :: Integer -> AgdaAny -> AgdaAny
du_const'8345'_208 :: Integer -> AgdaAny -> AgdaAny
du_const'8345'_208 Integer
v0 AgdaAny
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (let v3 :: t
v3 = (Integer -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> AgdaAny -> AgdaAny
du_const'8345'_208 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) in
              AgdaAny -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
forall a. a
v3)))