Documentation

type Pair a b = (a, b) Source #

d_Either_6 ∷ p → p → () Source #

type T_Either_6 a0 a1 = Either a0 a1 Source #

pattern C_inj'8321'_12 ∷ a → Either a b Source #

pattern C_inj'8322'_14 ∷ ∀ {a} {b}. b → Either a b Source #

check_inj'8321'_12 ∷ ∀ xA. ∀ xB. xA → T_Either_6 xA xB Source #

check_inj'8322'_14 ∷ ∀ xA. ∀ xB. xB → T_Either_6 xA xB Source #

cover_Either_6 ∷ Either a1 a2 → () Source #

d_either_22 ∷ () → () → () → T_Either_6 AgdaAny AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny Source #

du_either_22 ∷ T_Either_6 AgdaAny AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny Source #

d_eitherBind_42 ∷ () → () → () → T_Either_6 AgdaAny AgdaAny → (AgdaAny → T_Either_6 AgdaAny AgdaAny) → T_Either_6 AgdaAny AgdaAny Source #

du_eitherBind_42 ∷ T_Either_6 AgdaAny AgdaAny → (AgdaAny → T_Either_6 AgdaAny AgdaAny) → T_Either_6 AgdaAny AgdaAny Source #

d_decIf_56 ∷ () → () → T_Dec_20 → AgdaAny → AgdaAny → AgdaAny Source #

du_decIf_56 ∷ T_Dec_20 → AgdaAny → AgdaAny → AgdaAny Source #

d_cong'8323'_92 ∷ () → () → () → () → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'8801''45'subst'45'removable_114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #

d__'8724'_'8803'__120 ∷ p → p → p → () Source #

data T__'8724'_'8803'__120 Source #

d_unique'8724'_144 ∷ Integer → Integer → Integer → T__'8724'_'8803'__120 → T__'8724'_'8803'__120 → T__'8801'__12 Source #

d_'43'2'8724'_156 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8724'_'8803'__120 Source #

du_'43'2'8724'_156 ∷ Integer → T__'8724'_'8803'__120 Source #

d_'8724'2'43'_174 ∷ Integer → Integer → Integer → T__'8724'_'8803'__120 → T__'8801'__12 Source #

d_alldone_180 ∷ Integer → T__'8724'_'8803'__120 Source #

d_Monad_186 ∷ p → () Source #

data T_Monad_186 Source #

d_return_202 ∷ T_Monad_186 → () → AgdaAny → AgdaAny Source #

d__'62''62''61'__208 ∷ T_Monad_186 → () → () → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny Source #

d__'62''62'__214 ∷ (() → ()) → T_Monad_186 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'62''62'__214 ∷ T_Monad_186 → AgdaAny → AgdaAny → AgdaAny Source #

d_fmap_224 ∷ (() → ()) → T_Monad_186 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_fmap_224 ∷ T_Monad_186 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d__'62''62'__232 ∷ (() → ()) → T_Monad_186 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'62''62'__232 ∷ T_Monad_186 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

d__'62''62''61'__234 ∷ T_Monad_186 → () → () → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny Source #

d_fmap_236 ∷ (() → ()) → T_Monad_186 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_fmap_236 ∷ T_Monad_186 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_return_238 ∷ T_Monad_186 → () → AgdaAny → AgdaAny Source #

d_MaybeMonad_240 ∷ T_Monad_186 Source #

d_sumBind_248 ∷ () → () → () → T__'8846'__30 → (AgdaAny → T__'8846'__30) → T__'8846'__30 Source #

du_sumBind_248 ∷ T__'8846'__30 → (AgdaAny → T__'8846'__30) → T__'8846'__30 Source #

d_SumMonad_262 ∷ () → T_Monad_186 Source #

du_SumMonad_262 ∷ T_Monad_186 Source #

d_EitherMonad_268 ∷ () → T_Monad_186 Source #

du_EitherMonad_268 ∷ T_Monad_186 Source #

d_EitherP_274 ∷ () → T_Monad_186 Source #

du_EitherP_274 ∷ T_Monad_186 Source #

d_withE_282 ∷ () → () → () → (AgdaAny → AgdaAny) → T_Either_6 AgdaAny AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

du_withE_282 ∷ (AgdaAny → AgdaAny) → T_Either_6 AgdaAny AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

d_dec2Either_294 ∷ () → T_Dec_20 → T_Either_6 (AgdaAny → T_Irrelevant_20) AgdaAny Source #

du_dec2Either_294 ∷ T_Dec_20 → T_Either_6 (AgdaAny → T_Irrelevant_20) AgdaAny Source #

d_Writer_304 ∷ p → p → () Source #

data T_Writer_304 Source #

d_wrvalue_314 ∷ T_Writer_304 → AgdaAny Source #

d_accum_316 ∷ T_Writer_304 → AgdaAny Source #

d_WriterMonad_328 ∷ () → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_Monad_186 Source #

du_WriterMonad_328 ∷ AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_Monad_186 Source #

d_tell_344 ∷ () → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Writer_304 Source #

du_tell_344 ∷ AgdaAny → T_Writer_304 Source #

d_RuntimeError_348 ∷ () Source #

type T_RuntimeError_348 = RuntimeError Source #

pattern C_gasError_350 ∷ RuntimeError Source #

pattern C_userError_352 ∷ RuntimeError Source #

pattern C_runtimeTypeError_354 ∷ RuntimeError Source #

check_gasError_350 ∷ T_RuntimeError_348 Source #

check_userError_352 ∷ T_RuntimeError_348 Source #

check_runtimeTypeError_354 ∷ T_RuntimeError_348 Source #

cover_RuntimeError_348 ∷ RuntimeError → () Source #

type T_ByteString_356 = ByteString Source #

d_ByteString_356 ∷ a Source #

d_eqByteString_358 ∷ T_ByteString_356 → T_ByteString_356 → Bool Source #

d_mkByteString_360 ∷ a Source #

d__'215'__366 ∷ p → p → () Source #

type T__'215'__366 a0 a1 = Pair a0 a1 Source #

pattern C__'44'__380 ∷ a → b → (a, b) Source #

check__'44'__380 ∷ ∀ xA. ∀ xB. xA → xB → T__'215'__366 xA xB Source #

cover__'215'__366 ∷ Pair a1 a2 → () Source #

d_proj'8321'_376 ∷ T__'215'__366 AgdaAny AgdaAny → AgdaAny Source #

d_proj'8322'_378 ∷ T__'215'__366 AgdaAny AgdaAny → AgdaAny Source #

d_List_384 ∷ p → () Source #

type T_List_384 a0 = List a0 Source #

pattern C_'91''93'_388 ∷ [a] Source #

pattern C__'8759'__390 ∷ a → [a] → [a] Source #

check_'91''93'_388 ∷ ∀ xA. T_List_384 xA Source #

check__'8759'__390 ∷ ∀ xA. xA → T_List_384 xA → T_List_384 xA Source #

cover_List_384 ∷ List a1 → () Source #

d_length_394 ∷ () → T_List_384 AgdaAny → Integer Source #

du_length_394 ∷ T_List_384 AgdaAny → Integer Source #

d_map_404 ∷ () → () → (AgdaAny → AgdaAny) → T_List_384 AgdaAny → T_List_384 AgdaAny Source #

du_map_404 ∷ (AgdaAny → AgdaAny) → T_List_384 AgdaAny → T_List_384 AgdaAny Source #

d_toList_416 ∷ () → T_List_384 AgdaAny → [AgdaAny] Source #

du_toList_416 ∷ T_List_384 AgdaAny → [AgdaAny] Source #

d_fromList_424 ∷ () → [AgdaAny] → T_List_384 AgdaAny Source #

du_fromList_424 ∷ [AgdaAny] → T_List_384 AgdaAny Source #

d_dropLIST_432 ∷ () → Integer → T_List_384 AgdaAny → T_List_384 AgdaAny Source #

du_dropLIST_432 ∷ Integer → T_List_384 AgdaAny → T_List_384 AgdaAny Source #

d_drop_444 ∷ () → Integer → T_List_384 AgdaAny → () → Integer → T_List_384 AgdaAny → T_List_384 AgdaAny Source #

du_drop_444 ∷ Integer → T_List_384 AgdaAny → T_List_384 AgdaAny Source #

d_map'45'cong_468 ∷ () → () → [AgdaAny] → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #

d_DATA_478 ∷ () Source #

type T_DATA_478 = Data Source #

pattern C_ConstrDATA_480 ∷ Integer → [Data] → Data Source #

pattern C_MapDATA_482 ∷ [(Data, Data)] → Data Source #

pattern C_ListDATA_484 ∷ [Data] → Data Source #

pattern C_iDATA_486 ∷ Integer → Data Source #

pattern C_bDATA_488 ∷ ByteString → Data Source #

check_ConstrDATA_480 ∷ Integer → T_List_384 T_DATA_478 → T_DATA_478 Source #

check_MapDATA_482 ∷ T_List_384 (T__'215'__366 T_DATA_478 T_DATA_478) → T_DATA_478 Source #

check_ListDATA_484 ∷ T_List_384 T_DATA_478 → T_DATA_478 Source #

check_iDATA_486 ∷ Integer → T_DATA_478 Source #

check_bDATA_488 ∷ T_ByteString_356 → T_DATA_478 Source #

cover_DATA_478 ∷ Data → () Source #

d_eqDATA_490 ∷ T_DATA_478 → T_DATA_478 → Bool Source #

type T_Bls12'45'381'45'G1'45'Element_492 = Element Source #

d_Bls12'45'381'45'G1'45'Element_492 ∷ a Source #

d_eqBls12'45'381'45'G1'45'Element_494 ∷ T_Bls12'45'381'45'G1'45'Element_492 → T_Bls12'45'381'45'G1'45'Element_492 → Bool Source #

type T_Bls12'45'381'45'G2'45'Element_496 = Element Source #

d_Bls12'45'381'45'G2'45'Element_496 ∷ a Source #

d_eqBls12'45'381'45'G2'45'Element_498 ∷ T_Bls12'45'381'45'G2'45'Element_496 → T_Bls12'45'381'45'G2'45'Element_496 → Bool Source #

type T_Bls12'45'381'45'MlResult_500 = MlResult Source #

d_Bls12'45'381'45'MlResult_500 ∷ a Source #

d_eqBls12'45'381'45'MlResult_502 ∷ T_Bls12'45'381'45'MlResult_500 → T_Bls12'45'381'45'MlResult_500 → Bool Source #

d_Kind_504 ∷ () Source #

type T_Kind_504 = KIND Source #

pattern C_'42'_506 ∷ KIND Source #

pattern C_'9839'_508 ∷ KIND Source #

pattern C__'8658'__510 ∷ KIND → KIND → KIND Source #

check_'42'_506 ∷ T_Kind_504 Source #

check_'9839'_508 ∷ T_Kind_504 Source #

check__'8658'__510 ∷ T_Kind_504 → T_Kind_504 → T_Kind_504 Source #

cover_Kind_504 ∷ KIND → () Source #