{-# 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.Agda.Builtin.Sigma 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

-- Agda.Builtin.Sigma.Σ
d_Σ_14 :: p -> p -> p -> p -> ()
d_Σ_14 p
a0 p
a1 p
a2 p
a3 = ()
data T_Σ_14 = C__'44'__32 AgdaAny AgdaAny
-- Agda.Builtin.Sigma.Σ.fst
d_fst_28 :: T_Σ_14 -> AgdaAny
d_fst_28 :: T_Σ_14 -> AgdaAny
d_fst_28 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      C__'44'__32 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Agda.Builtin.Sigma.Σ.snd
d_snd_30 :: T_Σ_14 -> AgdaAny
d_snd_30 :: T_Σ_14 -> AgdaAny
d_snd_30 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      C__'44'__32 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError