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_is'45'inj'8321'_40 ∷ () → () → T_Either_6 AgdaAny AgdaAny → Bool Source #

du_is'45'inj'8321'_40 ∷ T_Either_6 AgdaAny AgdaAny → Bool Source #

d_is'45'inj'8322'_46 ∷ () → () → T_Either_6 AgdaAny AgdaAny → Bool Source #

du_is'45'inj'8322'_46 ∷ T_Either_6 AgdaAny AgdaAny → Bool Source #

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

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

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

du_decIf_68 ∷ T_Dec_20 → AgdaAny → AgdaAny → AgdaAny Source #

d_maybeToEither_86 ∷ () → () → AgdaAny → Maybe AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

du_maybeToEither_86 ∷ AgdaAny → Maybe AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

d_try_94 ∷ () → () → Maybe AgdaAny → AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

du_try_94 ∷ Maybe AgdaAny → AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

d_eitherToMaybe_104 ∷ () → () → T_Either_6 AgdaAny AgdaAny → Maybe AgdaAny Source #

du_eitherToMaybe_104 ∷ T_Either_6 AgdaAny AgdaAny → Maybe AgdaAny Source #

d_natToFin_110 ∷ Integer → Integer → Maybe T_Fin_10 Source #

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

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

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

d_unique'8724'_204 ∷ Integer → Integer → Integer → T__'8724'_'8803'__180 → T__'8724'_'8803'__180 → T__'8801'__12 Source #

d_'43'2'8724'_216 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8724'_'8803'__180 Source #

du_'43'2'8724'_216 ∷ Integer → T__'8724'_'8803'__180 Source #

d_'8724'2'43'_234 ∷ Integer → Integer → Integer → T__'8724'_'8803'__180 → T__'8801'__12 Source #

d_alldone_240 ∷ Integer → T__'8724'_'8803'__180 Source #

d_Monad_246 ∷ p → () Source #

data T_Monad_246 Source #

d_return_262 ∷ T_Monad_246 → () → AgdaAny → AgdaAny Source #

d__'62''62''61'__268 ∷ T_Monad_246 → () → () → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny Source #

d__'62''62'__274 ∷ (() → ()) → T_Monad_246 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'62''62'__274 ∷ T_Monad_246 → AgdaAny → AgdaAny → AgdaAny Source #

d_fmap_284 ∷ (() → ()) → T_Monad_246 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_fmap_284 ∷ T_Monad_246 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d__'62''62'__292 ∷ (() → ()) → T_Monad_246 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'62''62'__292 ∷ T_Monad_246 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

d__'62''62''61'__294 ∷ T_Monad_246 → () → () → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny Source #

d_fmap_296 ∷ (() → ()) → T_Monad_246 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_fmap_296 ∷ T_Monad_246 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_return_298 ∷ T_Monad_246 → () → AgdaAny → AgdaAny Source #

d_MaybeMonad_300 ∷ T_Monad_246 Source #

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

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

d_SumMonad_322 ∷ () → T_Monad_246 Source #

du_SumMonad_322 ∷ T_Monad_246 Source #

d_EitherMonad_328 ∷ () → T_Monad_246 Source #

du_EitherMonad_328 ∷ T_Monad_246 Source #

d_EitherP_334 ∷ () → T_Monad_246 Source #

du_EitherP_334 ∷ T_Monad_246 Source #

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

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

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

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

d_Writer_364 ∷ p → p → () Source #

data T_Writer_364 Source #

d_wrvalue_374 ∷ T_Writer_364 → AgdaAny Source #

d_accum_376 ∷ T_Writer_364 → AgdaAny Source #

d_WriterMonad_388 ∷ () → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_Monad_246 Source #

du_WriterMonad_388 ∷ AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_Monad_246 Source #

d_tell_404 ∷ () → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Writer_364 Source #

du_tell_404 ∷ AgdaAny → T_Writer_364 Source #

d_RuntimeError_408 ∷ () Source #

type T_RuntimeError_408 = RuntimeError Source #

pattern C_gasError_410 ∷ RuntimeError Source #

pattern C_userError_412 ∷ RuntimeError Source #

pattern C_runtimeTypeError_414 ∷ RuntimeError Source #

check_gasError_410 ∷ T_RuntimeError_408 Source #

check_userError_412 ∷ T_RuntimeError_408 Source #

check_runtimeTypeError_414 ∷ T_RuntimeError_408 Source #

cover_RuntimeError_408 ∷ RuntimeError → () Source #

type T_ByteString_416 = ByteString Source #

d_ByteString_416 ∷ a Source #

d_mkByteString_418 ∷ a Source #

d_eqByteString_420 ∷ T_ByteString_416 → T_ByteString_416 → Bool Source #

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

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

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

check__'44'__440 ∷ ∀ xA. ∀ xB. xA → xB → T__'215'__426 xA xB Source #

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

d_proj'8321'_436 ∷ T__'215'__426 AgdaAny AgdaAny → AgdaAny Source #

d_proj'8322'_438 ∷ T__'215'__426 AgdaAny AgdaAny → AgdaAny Source #

d_List_444 ∷ p → () Source #

type T_List_444 a0 = List a0 Source #

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

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

check_'91''93'_448 ∷ ∀ xA. T_List_444 xA Source #

check__'8759'__450 ∷ ∀ xA. xA → T_List_444 xA → T_List_444 xA Source #

cover_List_444 ∷ List a1 → () Source #

d_All_458 ∷ p → p → p → p → () Source #

data T_All_458 Source #

d_length_480 ∷ () → T_List_444 AgdaAny → Integer Source #

du_length_480 ∷ T_List_444 AgdaAny → Integer Source #

d_map_490 ∷ () → () → (AgdaAny → AgdaAny) → T_List_444 AgdaAny → T_List_444 AgdaAny Source #

du_map_490 ∷ (AgdaAny → AgdaAny) → T_List_444 AgdaAny → T_List_444 AgdaAny Source #

d_toList_502 ∷ () → T_List_444 AgdaAny → [AgdaAny] Source #

du_toList_502 ∷ T_List_444 AgdaAny → [AgdaAny] Source #

d_fromList_510 ∷ () → [AgdaAny] → T_List_444 AgdaAny Source #

du_fromList_510 ∷ [AgdaAny] → T_List_444 AgdaAny Source #

d_dropLIST_518 ∷ () → Integer → T_List_444 AgdaAny → T_List_444 AgdaAny Source #

du_dropLIST_518 ∷ Integer → T_List_444 AgdaAny → T_List_444 AgdaAny Source #

d_drop_530 ∷ () → Integer → T_List_444 AgdaAny → () → Integer → T_List_444 AgdaAny → T_List_444 AgdaAny Source #

du_drop_530 ∷ Integer → T_List_444 AgdaAny → T_List_444 AgdaAny Source #

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

d_sequence_570 ∷ () → (() → ()) → T_Monad_246 → T_List_444 AgdaAny → AgdaAny Source #

du_sequence_570 ∷ T_Monad_246 → T_List_444 AgdaAny → AgdaAny Source #

d_mapM_588 ∷ () → () → (() → ()) → T_Monad_246 → (AgdaAny → AgdaAny) → T_List_444 AgdaAny → AgdaAny Source #

du_mapM_588 ∷ T_Monad_246 → (AgdaAny → AgdaAny) → T_List_444 AgdaAny → AgdaAny Source #

type T_Array_592 a0 = Vector a0 Source #

d_Array_592 ∷ a Source #

d_HSlengthOfArray_596 ∷ ∀ xA. () → T_Array_592 xA → Integer Source #

d_HSlistToArray_600 ∷ ∀ xA. () → T_List_444 xA → T_Array_592 xA Source #

d_HSindexArray_602 ∷ ∀ xA. () → T_Array_592 xA → Integer → xA Source #

d_mkArray_606 ∷ a Source #

d_DATA_608 ∷ () Source #

type T_DATA_608 = Data Source #

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

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

pattern C_ListDATA_614 ∷ [Data] → Data Source #

pattern C_iDATA_616 ∷ Integer → Data Source #

pattern C_bDATA_618 ∷ ByteString → Data Source #

check_ConstrDATA_610 ∷ Integer → T_List_444 T_DATA_608 → T_DATA_608 Source #

check_MapDATA_612 ∷ T_List_444 (T__'215'__426 T_DATA_608 T_DATA_608) → T_DATA_608 Source #

check_ListDATA_614 ∷ T_List_444 T_DATA_608 → T_DATA_608 Source #

check_iDATA_616 ∷ Integer → T_DATA_608 Source #

check_bDATA_618 ∷ T_ByteString_416 → T_DATA_608 Source #

cover_DATA_608 ∷ Data → () Source #

d_eqDATA_620 ∷ T_DATA_608 → T_DATA_608 → Bool Source #

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

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

d_eqBls12'45'381'45'G1'45'Element_756 ∷ T_Bls12'45'381'45'G1'45'Element_754 → T_Bls12'45'381'45'G1'45'Element_754 → Bool Source #

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

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

d_eqBls12'45'381'45'G2'45'Element_760 ∷ T_Bls12'45'381'45'G2'45'Element_758 → T_Bls12'45'381'45'G2'45'Element_758 → Bool Source #

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

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

d_eqBls12'45'381'45'MlResult_764 ∷ T_Bls12'45'381'45'MlResult_762 → T_Bls12'45'381'45'MlResult_762 → Bool Source #

d_Kind_766 ∷ () Source #

type T_Kind_766 = KIND Source #

pattern C_'42'_768 ∷ KIND Source #

pattern C_'9839'_770 ∷ KIND Source #

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

check_'42'_768 ∷ T_Kind_766 Source #

check_'9839'_770 ∷ T_Kind_766 Source #

check__'8658'__772 ∷ T_Kind_766 → T_Kind_766 → T_Kind_766 Source #

cover_Kind_766 ∷ KIND → () Source #