{-# 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.Algebra.Consequences.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.Primitive
import qualified MAlonzo.Code.Data.Sum.Base

-- Algebra.Consequences.Base.sel⇒idem
d_sel'8658'idem_16 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny
d_sel'8658'idem_16 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
d_sel'8658'idem_16 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> AgdaAny
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 AgdaAny -> AgdaAny -> T__'8846'__30
v5 AgdaAny
v6
  = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
du_sel'8658'idem_16 AgdaAny -> AgdaAny -> T__'8846'__30
v5 AgdaAny
v6
du_sel'8658'idem_16 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny
du_sel'8658'idem_16 :: (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
du_sel'8658'idem_16 AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v1
  = let v2 :: t
v2 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v1 AgdaAny
v1 in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall {t}. t
v2 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
         T__'8846'__30
_ -> AgdaAny
forall {t}. t
MAlonzo.RTE.mazUnreachableError)