{-# 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.Maybe.Properties 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.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Maybe.Relation.Unary.All
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
d_just'45'injective_22 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_just'45'injective_22 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_just'45'injective_22 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_'8801''45'dec_24 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
Maybe AgdaAny ->
Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8801''45'dec_24 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T_Dec_32
d_'8801''45'dec_24 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 Maybe AgdaAny
v3 Maybe AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8801''45'dec_24 AgdaAny -> AgdaAny -> T_Dec_32
v2 Maybe AgdaAny
v3 Maybe AgdaAny
v4
du_'8801''45'dec_24 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
Maybe AgdaAny ->
Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8801''45'dec_24 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
du_'8801''45'dec_24 AgdaAny -> AgdaAny -> T_Dec_32
v0 Maybe AgdaAny
v1 Maybe AgdaAny
v2
= case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
-> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
-> ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
AgdaAny
forall a. a
erased ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v3 AgdaAny
v4)
Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> (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)
Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3
-> (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)
Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> (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
forall a. a
erased)
Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_map'45'id_42 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'id_42 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_map'45'id_42 = T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
d_map'45'id'8322'_52 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
Maybe AgdaAny ->
MAlonzo.Code.Data.Maybe.Relation.Unary.All.T_All_18 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'id'8322'_52 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
d_map'45'id'8322'_52 = T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
forall a. a
erased
d_map'45''60''8739''62''45'commute_62 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
Maybe AgdaAny ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45''60''8739''62''45'commute_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
d_map'45''60''8739''62''45'commute_62 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
d_map'45'cong_78 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'cong_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T__'8801'__12
d_map'45'cong_78 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
d_map'45'cong'8322'_94 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) ->
Maybe AgdaAny ->
MAlonzo.Code.Data.Maybe.Relation.Unary.All.T_All_18 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'cong'8322'_94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
d_map'45'cong'8322'_94 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_All_18
-> T__'8801'__12
forall a. a
erased
d_map'45'injective_100 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
Maybe AgdaAny ->
Maybe AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'injective_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_map'45'injective_100 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_map'45'compose_118 ::
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) ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'compose_118 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_map'45'compose_118 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
d_map'45'nothing_126 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
Maybe AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'nothing_126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_map'45'nothing_126 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_map'45'just_134 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
Maybe AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'just_134 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_map'45'just_134 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_maybe'45'map_148 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(Maybe AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
AgdaAny ->
(AgdaAny -> AgdaAny) ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_maybe'45'map_148 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_maybe'45'map_148 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
d_maybe'8242''45'map_172 ::
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) ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_maybe'8242''45'map_172 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_maybe'8242''45'map_172 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
d_Associative_202 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Associative_202 :: T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Associative_202 = T_Level_18
-> T_Level_18
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
d_Identity_218 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny ->
(Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_Identity_218 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_Identity_218 = T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
d_LeftIdentity_232 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny ->
(Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_LeftIdentity_232 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_LeftIdentity_232 = T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
d_RightIdentity_244 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny ->
(Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> ()
d_RightIdentity_244 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
d_RightIdentity_244 = T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
d_'60''8739''62''45'assoc_254 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny ->
Maybe AgdaAny ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'assoc_254 :: T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
d_'60''8739''62''45'assoc_254 = T_Level_18
-> T_Level_18
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
d_'60''8739''62''45'identity'737'_266 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'identity'737'_266 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'identity'737'_266 = T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
d_'60''8739''62''45'identity'691'_270 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''8739''62''45'identity'691'_270 :: T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
d_'60''8739''62''45'identity'691'_270 = T_Level_18 -> T_Level_18 -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
d_'60''8739''62''45'identity_274 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''8739''62''45'identity_274 :: T_Level_18 -> T_Level_18 -> T_Σ_14
d_'60''8739''62''45'identity_274 ~T_Level_18
v0 ~T_Level_18
v1
= T_Σ_14
du_'60''8739''62''45'identity_274
du_'60''8739''62''45'identity_274 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''8739''62''45'identity_274 :: T_Σ_14
du_'60''8739''62''45'identity_274
= (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
d_IsMagma_316 :: p -> p -> p -> T_Level_18
d_IsMagma_316 p
a0 p
a1 p
a2 = ()
d_IsMonoid_318 :: p -> p -> p -> p -> T_Level_18
d_IsMonoid_318 p
a0 p
a1 p
a2 p
a3 = ()
d_IsSemigroup_326 :: p -> p -> p -> T_Level_18
d_IsSemigroup_326 p
a0 p
a1 p
a2 = ()
d_'60''8739''62''45'isMagma_1708 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Algebra.Structures.T_IsMagma_86
d_'60''8739''62''45'isMagma_1708 :: T_Level_18 -> T_Level_18 -> T_IsMagma_86
d_'60''8739''62''45'isMagma_1708 ~T_Level_18
v0 ~T_Level_18
v1
= T_IsMagma_86
du_'60''8739''62''45'isMagma_1708
du_'60''8739''62''45'isMagma_1708 ::
MAlonzo.Code.Algebra.Structures.T_IsMagma_86
du_'60''8739''62''45'isMagma_1708 :: T_IsMagma_86
du_'60''8739''62''45'isMagma_1708
= (T_IsEquivalence_26
-> (AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> T_IsMagma_86
forall a b. a -> b
coe
T_IsEquivalence_26
-> (AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
(T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
AgdaAny
forall a. a
erased
d_'60''8739''62''45'isSemigroup_1710 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
d_'60''8739''62''45'isSemigroup_1710 :: T_Level_18 -> T_Level_18 -> T_IsSemigroup_194
d_'60''8739''62''45'isSemigroup_1710 ~T_Level_18
v0 ~T_Level_18
v1
= T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710
du_'60''8739''62''45'isSemigroup_1710 ::
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710 :: T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710
= (T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> T_IsSemigroup_194
forall a b. a -> b
coe
T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
(T_IsMagma_86 -> AgdaAny
forall a b. a -> b
coe T_IsMagma_86
du_'60''8739''62''45'isMagma_1708) AgdaAny
forall a. a
erased
d_'60''8739''62''45'isMonoid_1712 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_'60''8739''62''45'isMonoid_1712 :: T_Level_18 -> T_Level_18 -> T_IsMonoid_358
d_'60''8739''62''45'isMonoid_1712 ~T_Level_18
v0 ~T_Level_18
v1
= T_IsMonoid_358
du_'60''8739''62''45'isMonoid_1712
du_'60''8739''62''45'isMonoid_1712 ::
MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
du_'60''8739''62''45'isMonoid_1712 :: T_IsMonoid_358
du_'60''8739''62''45'isMonoid_1712
= (T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny -> T_IsMonoid_358
forall a b. a -> b
coe
T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_7687
(T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710)
(T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
du_'60''8739''62''45'identity_274)
d_'60''8739''62''45'semigroup_1714 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
d_'60''8739''62''45'semigroup_1714 :: T_Level_18 -> T_Level_18 -> T_Semigroup_206
d_'60''8739''62''45'semigroup_1714 ~T_Level_18
v0 ~T_Level_18
v1
= T_Semigroup_206
du_'60''8739''62''45'semigroup_1714
du_'60''8739''62''45'semigroup_1714 ::
MAlonzo.Code.Algebra.Bundles.T_Semigroup_206
du_'60''8739''62''45'semigroup_1714 :: T_Semigroup_206
du_'60''8739''62''45'semigroup_1714
= ((AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> T_Semigroup_206)
-> AgdaAny -> AgdaAny -> T_Semigroup_206
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsSemigroup_194 -> T_Semigroup_206
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_3669
((Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du__'60''8739''62'__84)
(T_IsSemigroup_194 -> AgdaAny
forall a b. a -> b
coe T_IsSemigroup_194
du_'60''8739''62''45'isSemigroup_1710)
d_'60''8739''62''45'monoid_1716 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Algebra.Bundles.T_Monoid_506
d_'60''8739''62''45'monoid_1716 :: T_Level_18 -> T_Level_18 -> T_Monoid_506
d_'60''8739''62''45'monoid_1716 ~T_Level_18
v0 ~T_Level_18
v1
= T_Monoid_506
du_'60''8739''62''45'monoid_1716
du_'60''8739''62''45'monoid_1716 ::
MAlonzo.Code.Algebra.Bundles.T_Monoid_506
du_'60''8739''62''45'monoid_1716 :: T_Monoid_506
du_'60''8739''62''45'monoid_1716
= ((AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_358 -> T_Monoid_506)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Monoid_506
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_IsMonoid_358 -> T_Monoid_506
MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_8851
((Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du__'60''8739''62'__84)
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
(T_IsMonoid_358 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_358
du_'60''8739''62''45'isMonoid_1712)