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_maybeToEither_74 ∷ () → () → AgdaAny → Maybe AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

du_maybeToEither_74 ∷ AgdaAny → Maybe AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

d_natToFin_80 ∷ Integer → Integer → Maybe T_Fin_10 Source #

d_cong'8323'_122 ∷ () → () → () → () → (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_144 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #

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

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

d_unique'8724'_174 ∷ Integer → Integer → Integer → T__'8724'_'8803'__150 → T__'8724'_'8803'__150 → T__'8801'__12 Source #

d_'43'2'8724'_186 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8724'_'8803'__150 Source #

du_'43'2'8724'_186 ∷ Integer → T__'8724'_'8803'__150 Source #

d_'8724'2'43'_204 ∷ Integer → Integer → Integer → T__'8724'_'8803'__150 → T__'8801'__12 Source #

d_alldone_210 ∷ Integer → T__'8724'_'8803'__150 Source #

d_Monad_216 ∷ p → () Source #

data T_Monad_216 Source #

d_return_232 ∷ T_Monad_216 → () → AgdaAny → AgdaAny Source #

d__'62''62''61'__238 ∷ T_Monad_216 → () → () → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny Source #

d__'62''62'__244 ∷ (() → ()) → T_Monad_216 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'62''62'__244 ∷ T_Monad_216 → AgdaAny → AgdaAny → AgdaAny Source #

d_fmap_254 ∷ (() → ()) → T_Monad_216 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_fmap_254 ∷ T_Monad_216 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d__'62''62'__262 ∷ (() → ()) → T_Monad_216 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'62''62'__262 ∷ T_Monad_216 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

d__'62''62''61'__264 ∷ T_Monad_216 → () → () → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny Source #

d_fmap_266 ∷ (() → ()) → T_Monad_216 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_fmap_266 ∷ T_Monad_216 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_return_268 ∷ T_Monad_216 → () → AgdaAny → AgdaAny Source #

d_MaybeMonad_270 ∷ T_Monad_216 Source #

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

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

d_SumMonad_292 ∷ () → T_Monad_216 Source #

du_SumMonad_292 ∷ T_Monad_216 Source #

d_EitherMonad_298 ∷ () → T_Monad_216 Source #

du_EitherMonad_298 ∷ T_Monad_216 Source #

d_EitherP_304 ∷ () → T_Monad_216 Source #

du_EitherP_304 ∷ T_Monad_216 Source #

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

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

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

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

d_Writer_334 ∷ p → p → () Source #

data T_Writer_334 Source #

d_wrvalue_344 ∷ T_Writer_334 → AgdaAny Source #

d_accum_346 ∷ T_Writer_334 → AgdaAny Source #

d_WriterMonad_358 ∷ () → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_Monad_216 Source #

du_WriterMonad_358 ∷ AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_Monad_216 Source #

d_tell_374 ∷ () → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Writer_334 Source #

du_tell_374 ∷ AgdaAny → T_Writer_334 Source #

d_RuntimeError_378 ∷ () Source #

type T_RuntimeError_378 = RuntimeError Source #

pattern C_gasError_380 ∷ RuntimeError Source #

pattern C_userError_382 ∷ RuntimeError Source #

pattern C_runtimeTypeError_384 ∷ RuntimeError Source #

check_gasError_380 ∷ T_RuntimeError_378 Source #

check_userError_382 ∷ T_RuntimeError_378 Source #

check_runtimeTypeError_384 ∷ T_RuntimeError_378 Source #

cover_RuntimeError_378 ∷ RuntimeError → () Source #

type T_ByteString_386 = ByteString Source #

d_ByteString_386 ∷ a Source #

d_mkByteString_388 ∷ a Source #

d_eqByteString_390 ∷ T_ByteString_386 → T_ByteString_386 → Bool Source #

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

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

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

check__'44'__410 ∷ ∀ xA. ∀ xB. xA → xB → T__'215'__396 xA xB Source #

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

d_proj'8321'_406 ∷ T__'215'__396 AgdaAny AgdaAny → AgdaAny Source #

d_proj'8322'_408 ∷ T__'215'__396 AgdaAny AgdaAny → AgdaAny Source #

d_List_414 ∷ p → () Source #

type T_List_414 a0 = List a0 Source #

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

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

check_'91''93'_418 ∷ ∀ xA. T_List_414 xA Source #

check__'8759'__420 ∷ ∀ xA. xA → T_List_414 xA → T_List_414 xA Source #

cover_List_414 ∷ List a1 → () Source #

d_length_424 ∷ () → T_List_414 AgdaAny → Integer Source #

du_length_424 ∷ T_List_414 AgdaAny → Integer Source #

d_map_434 ∷ () → () → (AgdaAny → AgdaAny) → T_List_414 AgdaAny → T_List_414 AgdaAny Source #

du_map_434 ∷ (AgdaAny → AgdaAny) → T_List_414 AgdaAny → T_List_414 AgdaAny Source #

d_toList_446 ∷ () → T_List_414 AgdaAny → [AgdaAny] Source #

du_toList_446 ∷ T_List_414 AgdaAny → [AgdaAny] Source #

d_fromList_454 ∷ () → [AgdaAny] → T_List_414 AgdaAny Source #

du_fromList_454 ∷ [AgdaAny] → T_List_414 AgdaAny Source #

d_dropLIST_462 ∷ () → Integer → T_List_414 AgdaAny → T_List_414 AgdaAny Source #

du_dropLIST_462 ∷ Integer → T_List_414 AgdaAny → T_List_414 AgdaAny Source #

d_drop_474 ∷ () → Integer → T_List_414 AgdaAny → () → Integer → T_List_414 AgdaAny → T_List_414 AgdaAny Source #

du_drop_474 ∷ Integer → T_List_414 AgdaAny → T_List_414 AgdaAny Source #

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

type T_Array_508 a0 = Vector a0 Source #

d_Array_508 ∷ a Source #

d_HSlengthOfArray_512 ∷ ∀ xA. () → T_Array_508 xA → Integer Source #

d_HSlistToArray_516 ∷ ∀ xA. () → T_List_414 xA → T_Array_508 xA Source #

d_HSindexArray_518 ∷ ∀ xA. () → T_Array_508 xA → Integer → xA Source #

d_mkArray_522 ∷ a Source #

d_DATA_524 ∷ () Source #

type T_DATA_524 = Data Source #

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

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

pattern C_ListDATA_530 ∷ [Data] → Data Source #

pattern C_iDATA_532 ∷ Integer → Data Source #

pattern C_bDATA_534 ∷ ByteString → Data Source #

check_ConstrDATA_526 ∷ Integer → T_List_414 T_DATA_524 → T_DATA_524 Source #

check_MapDATA_528 ∷ T_List_414 (T__'215'__396 T_DATA_524 T_DATA_524) → T_DATA_524 Source #

check_ListDATA_530 ∷ T_List_414 T_DATA_524 → T_DATA_524 Source #

check_iDATA_532 ∷ Integer → T_DATA_524 Source #

check_bDATA_534 ∷ T_ByteString_386 → T_DATA_524 Source #

cover_DATA_524 ∷ Data → () Source #

d_eqDATA_536 ∷ T_DATA_524 → T_DATA_524 → Bool Source #

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

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

d_eqBls12'45'381'45'G1'45'Element_672 ∷ T_Bls12'45'381'45'G1'45'Element_670 → T_Bls12'45'381'45'G1'45'Element_670 → Bool Source #

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

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

d_eqBls12'45'381'45'G2'45'Element_676 ∷ T_Bls12'45'381'45'G2'45'Element_674 → T_Bls12'45'381'45'G2'45'Element_674 → Bool Source #

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

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

d_eqBls12'45'381'45'MlResult_680 ∷ T_Bls12'45'381'45'MlResult_678 → T_Bls12'45'381'45'MlResult_678 → Bool Source #

d_Kind_682 ∷ () Source #

type T_Kind_682 = KIND Source #

pattern C_'42'_684 ∷ KIND Source #

pattern C_'9839'_686 ∷ KIND Source #

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

check_'42'_684 ∷ T_Kind_682 Source #

check_'9839'_686 ∷ T_Kind_682 Source #

check__'8658'__688 ∷ T_Kind_682 → T_Kind_682 → T_Kind_682 Source #

cover_Kind_682 ∷ KIND → () Source #