| Safe Haskell | None |
|---|
MAlonzo.Code.Codata.Musical.Colist.Base
Documentation
data AgdaColist a Source #
Constructors
| Nil | |
| Cons a (Inf (AgdaColist a)) |
type AgdaColist' l a = AgdaColist a Source #
d_Colist_20 :: p1 -> p2 -> () Source #
type T_Colist_20 a0 a1 = AgdaColist' a0 a1 Source #
pattern C_'91''93'_24 :: forall a. AgdaColist a Source #
pattern C__'8759'__30 :: forall a. a -> Inf (AgdaColist a) -> AgdaColist a Source #
check_'91''93'_24 :: forall xa. forall xA. T_Colist_20 xa xA Source #
check__'8759'__30 :: forall xa. forall xA. xA -> Infinity xa (T_Colist_20 xa xA) -> T_Colist_20 xa xA Source #
cover_Colist_20 :: AgdaColist' a1 a2 -> () Source #
d_null_32 :: T_Level_14 -> () -> T_Colist_20 AgdaAny AgdaAny -> Bool Source #
du_null_32 :: T_Colist_20 AgdaAny AgdaAny -> Bool Source #
d_length_34 :: T_Level_14 -> () -> T_Colist_20 AgdaAny AgdaAny -> T_Coℕ_8 Source #
du_length_34 :: T_Level_14 -> T_Colist_20 AgdaAny AgdaAny -> T_Coℕ_8 Source #
d_map_40 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
du_map_40 :: T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
d_fromList_50 :: T_Level_14 -> () -> [AgdaAny] -> T_Colist_20 AgdaAny AgdaAny Source #
du_fromList_50 :: T_Level_14 -> [AgdaAny] -> T_Colist_20 AgdaAny AgdaAny Source #
d_replicate_56 :: T_Level_14 -> () -> T_Coℕ_8 -> AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
du_replicate_56 :: T_Level_14 -> T_Coℕ_8 -> AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
d_lookup_64 :: T_Level_14 -> () -> Integer -> T_Colist_20 AgdaAny AgdaAny -> Maybe AgdaAny Source #
du_lookup_64 :: Integer -> T_Colist_20 AgdaAny AgdaAny -> Maybe AgdaAny Source #
d__'43''43'__78 :: T_Level_14 -> () -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
du__'43''43'__78 :: T_Level_14 -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
d__'8910'__88 :: T_Level_14 -> () -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
du__'8910'__88 :: T_Level_14 -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
d_concat_98 :: T_Level_14 -> () -> T_Colist_20 AgdaAny T_List'8314'_24 -> T_Colist_20 AgdaAny AgdaAny Source #
du_concat_98 :: T_Level_14 -> T_Colist_20 AgdaAny T_List'8314'_24 -> T_Colist_20 AgdaAny AgdaAny Source #
d_'91'_'93'_112 :: T_Level_14 -> () -> AgdaAny -> T_Colist_20 AgdaAny AgdaAny Source #
d_'9839''45'0_645 :: T_Level_14 -> () -> AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) -> Infinity AgdaAny T_Coℕ_8 Source #
du_'9839''45'0_645 :: T_Level_14 -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) -> Infinity AgdaAny T_Coℕ_8 Source #
d_'9839''45'1_1397 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
du_'9839''45'1_1397 :: T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
d_'9839''45'2_2287 :: T_Level_14 -> () -> AgdaAny -> [AgdaAny] -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
du_'9839''45'2_2287 :: T_Level_14 -> [AgdaAny] -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
d_'9839''45'3_2813 :: T_Level_14 -> () -> Infinity AgdaAny T_Coℕ_8 -> AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
du_'9839''45'3_2813 :: T_Level_14 -> Infinity AgdaAny T_Coℕ_8 -> AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
d_'9839''45'4_4093 :: T_Level_14 -> () -> AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) -> T_Colist_20 AgdaAny AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
du_'9839''45'4_4093 :: T_Level_14 -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) -> T_Colist_20 AgdaAny AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
d_'9839''45'5_4775 :: T_Level_14 -> () -> AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) -> T_Colist_20 AgdaAny AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
du_'9839''45'5_4775 :: T_Level_14 -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) -> T_Colist_20 AgdaAny AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
d_'9839''45'6_5519 :: T_Level_14 -> () -> AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny T_List'8314'_24) -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
du_'9839''45'6_5519 :: T_Level_14 -> Infinity AgdaAny (T_Colist_20 AgdaAny T_List'8314'_24) -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
d_'9839''45'7_5947 :: T_Level_14 -> () -> AgdaAny -> AgdaAny -> [AgdaAny] -> Infinity AgdaAny (T_Colist_20 AgdaAny T_List'8314'_24) -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
du_'9839''45'7_5947 :: T_Level_14 -> AgdaAny -> [AgdaAny] -> Infinity AgdaAny (T_Colist_20 AgdaAny T_List'8314'_24) -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #
d_'9839''45'8_6701 :: T_Level_14 -> () -> AgdaAny -> Infinity AgdaAny (T_Colist_20 AgdaAny AgdaAny) Source #