{-# 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.Data.Sum.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.Bool
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d__'8846'__30 :: p -> p -> p -> p -> ()
d__'8846'__30 p
a0 p
a1 p
a2 p
a3 = ()
data T__'8846'__30
= C_inj'8321'_38 AgdaAny | C_inj'8322'_42 AgdaAny
d_'91'_'44'_'93'_52 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(T__'8846'__30 -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
d_'91'_'44'_'93'_52 :: ()
-> ()
-> ()
-> ()
-> ()
-> (T__'8846'__30 -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> AgdaAny
d_'91'_'44'_'93'_52 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~T__'8846'__30 -> ()
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 T__'8846'__30
v8
= (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93'_52 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 T__'8846'__30
v8
du_'91'_'44'_'93'_52 ::
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93'_52 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93'_52 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T__'8846'__30
v2
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
C_inj'8321'_38 AgdaAny
v3 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3
C_inj'8322'_42 AgdaAny
v3 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3
T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'91'_'44'_'93''8242'_66 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
d_'91'_'44'_'93''8242'_66 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> AgdaAny
d_'91'_'44'_'93''8242'_66 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5
= (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66
du_'91'_'44'_'93''8242'_66 ::
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66 = ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93'_52
d_fromInj'8321'_68 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
d_fromInj'8321'_68 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> AgdaAny
d_fromInj'8321'_68 ~()
v0 ~()
v1 ~()
v2 ~()
v3 = (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_fromInj'8321'_68
du_fromInj'8321'_68 ::
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_fromInj'8321'_68 :: (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_fromInj'8321'_68 = ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66 (\ AgdaAny
v0 -> AgdaAny
v0)
d_fromInj'8322'_72 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
d_fromInj'8322'_72 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> AgdaAny
d_fromInj'8322'_72 ~()
v0 ~()
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny
v4 = (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_fromInj'8322'_72 AgdaAny -> AgdaAny
v4
du_fromInj'8322'_72 ::
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_fromInj'8322'_72 :: (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_fromInj'8322'_72 AgdaAny -> AgdaAny
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66 AgdaAny -> AgdaAny
v0 (\ AgdaAny
v1 -> AgdaAny
v1)
d_reduce_76 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T__'8846'__30 -> AgdaAny
d_reduce_76 :: () -> () -> T__'8846'__30 -> AgdaAny
d_reduce_76 ~()
v0 ~()
v1 = T__'8846'__30 -> AgdaAny
du_reduce_76
du_reduce_76 :: T__'8846'__30 -> AgdaAny
du_reduce_76 :: T__'8846'__30 -> AgdaAny
du_reduce_76
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66 (\ AgdaAny
v0 -> AgdaAny
v0) (\ AgdaAny
v0 -> AgdaAny
v0)
d_swap_78 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T__'8846'__30 -> T__'8846'__30
d_swap_78 :: () -> () -> () -> () -> T__'8846'__30 -> T__'8846'__30
d_swap_78 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T__'8846'__30
v4 = T__'8846'__30 -> T__'8846'__30
du_swap_78 T__'8846'__30
v4
du_swap_78 :: T__'8846'__30 -> T__'8846'__30
du_swap_78 :: T__'8846'__30 -> T__'8846'__30
du_swap_78 T__'8846'__30
v0
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
C_inj'8321'_38 AgdaAny
v1 -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8322'_42 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
C_inj'8322'_42 AgdaAny
v1 -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
T__'8846'__30
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
d_map_84 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
d_map_84 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
d_map_84 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny
v9 = (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map_84 AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny
v9
du_map_84 ::
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map_84 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map_84 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66 (\ AgdaAny
v2 -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8321'_38 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2))
(\ AgdaAny
v2 -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8322'_42 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2))
d_map'8321'_90 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
d_map'8321'_90 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
d_map'8321'_90 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 AgdaAny -> AgdaAny
v6 = (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map'8321'_90 AgdaAny -> AgdaAny
v6
du_map'8321'_90 ::
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map'8321'_90 :: (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map'8321'_90 AgdaAny -> AgdaAny
v0 = ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map_84 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
d_map'8322'_94 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
d_map'8322'_94 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
d_map'8322'_94 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 = (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map'8322'_94
du_map'8322'_94 ::
(AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map'8322'_94 :: (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map'8322'_94 = ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T__'8846'__30
-> T__'8846'__30
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map_84 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0))
d_assoc'691'_96 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T__'8846'__30 -> T__'8846'__30
d_assoc'691'_96 :: () -> () -> () -> () -> () -> () -> T__'8846'__30 -> T__'8846'__30
d_assoc'691'_96 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 = T__'8846'__30 -> T__'8846'__30
du_assoc'691'_96
du_assoc'691'_96 :: T__'8846'__30 -> T__'8846'__30
du_assoc'691'_96 :: T__'8846'__30 -> T__'8846'__30
du_assoc'691'_96
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66
(((AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map'8322'_94 ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8321'_38))
(((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 -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8322'_42) ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8322'_42))
d_assoc'737'_98 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T__'8846'__30 -> T__'8846'__30
d_assoc'737'_98 :: () -> () -> () -> () -> () -> () -> T__'8846'__30 -> T__'8846'__30
d_assoc'737'_98 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 = T__'8846'__30 -> T__'8846'__30
du_assoc'737'_98
du_assoc'737'_98 :: T__'8846'__30 -> T__'8846'__30
du_assoc'737'_98 :: T__'8846'__30 -> T__'8846'__30
du_assoc'737'_98
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
du_'91'_'44'_'93''8242'_66
(((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 -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8321'_38) ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8321'_38))
(((AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
du_map'8321'_90 ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
C_inj'8322'_42))
d__'45''8846''45'__100 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d__'45''8846''45'__100 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
d__'45''8846''45'__100 = ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased
d_fromDec_106 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Relation.Nullary.T_Dec_32 -> T__'8846'__30
d_fromDec_106 :: () -> () -> T_Dec_32 -> T__'8846'__30
d_fromDec_106 ~()
v0 ~()
v1 T_Dec_32
v2 = T_Dec_32 -> T__'8846'__30
du_fromDec_106 T_Dec_32
v2
du_fromDec_106 ::
MAlonzo.Code.Relation.Nullary.T_Dec_32 -> T__'8846'__30
du_fromDec_106 :: T_Dec_32 -> T__'8846'__30
du_fromDec_106 T_Dec_32
v0
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
AgdaAny -> T__'8846'__30
C_inj'8321'_38
((T_Reflects_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_14 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v2))
else (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
AgdaAny -> T__'8846'__30
C_inj'8322'_42
((T_Reflects_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_14 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v2))
T_Dec_32
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toDec_112 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T__'8846'__30 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_toDec_112 :: () -> () -> T__'8846'__30 -> T_Dec_32
d_toDec_112 ~()
v0 ~()
v1 T__'8846'__30
v2 = T__'8846'__30 -> T_Dec_32
du_toDec_112 T__'8846'__30
v2
du_toDec_112 ::
T__'8846'__30 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_toDec_112 :: T__'8846'__30 -> T_Dec_32
du_toDec_112 T__'8846'__30
v0
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
C_inj'8321'_38 AgdaAny
v1
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
C_inj'8322'_42 AgdaAny
v1
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8846'__30
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError