{-# 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
d_Σ_14 :: p -> p -> p -> p -> ()
d_Σ_14 p
a0 p
a1 p
a2 p
a3 = ()
data T_Σ_14 = C__'44'__32 AgdaAny AgdaAny
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
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