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__'60''124''62'__84 ∷ () → Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny Source #

du__'60''124''62'__84 ∷ Maybe AgdaAny → Maybe AgdaAny → Maybe AgdaAny Source #

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

du_maybeToEither_94 ∷ AgdaAny → Maybe AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

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

du_try_102 ∷ Maybe AgdaAny → AgdaAny → T_Either_6 AgdaAny AgdaAny Source #

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

du_eitherToMaybe_112 ∷ T_Either_6 AgdaAny AgdaAny → Maybe AgdaAny Source #

d_natToFin_118 ∷ Integer → Integer → Maybe T_Fin_10 Source #

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

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

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

d_unique'8724'_212 ∷ Integer → Integer → Integer → T__'8724'_'8803'__188 → T__'8724'_'8803'__188 → T__'8801'__12 Source #

d_'43'2'8724'_224 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8724'_'8803'__188 Source #

du_'43'2'8724'_224 ∷ Integer → T__'8724'_'8803'__188 Source #

d_'8724'2'43'_242 ∷ Integer → Integer → Integer → T__'8724'_'8803'__188 → T__'8801'__12 Source #

d_alldone_248 ∷ Integer → T__'8724'_'8803'__188 Source #

d_Monad_254 ∷ p → () Source #

data T_Monad_254 Source #

d_return_270 ∷ T_Monad_254 → () → AgdaAny → AgdaAny Source #

d__'62''62''61'__276 ∷ T_Monad_254 → () → () → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny Source #

d__'62''62'__282 ∷ (() → ()) → T_Monad_254 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'62''62'__282 ∷ T_Monad_254 → AgdaAny → AgdaAny → AgdaAny Source #

d_fmap_292 ∷ (() → ()) → T_Monad_254 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_fmap_292 ∷ T_Monad_254 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d__'62''62'__302 ∷ (() → ()) → T_Monad_254 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

du__'62''62'__302 ∷ T_Monad_254 → () → () → AgdaAny → AgdaAny → AgdaAny Source #

d__'62''62''61'__304 ∷ T_Monad_254 → () → () → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny Source #

d_fmap_306 ∷ (() → ()) → T_Monad_254 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_fmap_306 ∷ T_Monad_254 → () → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_return_308 ∷ T_Monad_254 → () → AgdaAny → AgdaAny Source #

d_MaybeMonad_310 ∷ T_Monad_254 Source #

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

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

d_SumMonad_332 ∷ () → T_Monad_254 Source #

du_SumMonad_332 ∷ T_Monad_254 Source #

d_EitherMonad_338 ∷ () → T_Monad_254 Source #

du_EitherMonad_338 ∷ T_Monad_254 Source #

d_EitherP_344 ∷ () → T_Monad_254 Source #

du_EitherP_344 ∷ T_Monad_254 Source #

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

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

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

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

d_Writer_374 ∷ p → p → () Source #

data T_Writer_374 Source #

d_wrvalue_384 ∷ T_Writer_374 → AgdaAny Source #

d_accum_386 ∷ T_Writer_374 → AgdaAny Source #

d_WriterMonad_398 ∷ () → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_Monad_254 Source #

du_WriterMonad_398 ∷ AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_Monad_254 Source #

d_tell_414 ∷ () → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Writer_374 Source #

du_tell_414 ∷ AgdaAny → T_Writer_374 Source #

d_RuntimeError_418 ∷ () Source #

type T_RuntimeError_418 = RuntimeError Source #

pattern C_gasError_420 ∷ RuntimeError Source #

pattern C_userError_422 ∷ RuntimeError Source #

pattern C_runtimeTypeError_424 ∷ RuntimeError Source #

check_gasError_420 ∷ T_RuntimeError_418 Source #

check_userError_422 ∷ T_RuntimeError_418 Source #

check_runtimeTypeError_424 ∷ T_RuntimeError_418 Source #

cover_RuntimeError_418 ∷ RuntimeError → () Source #

type T_ByteString_426 = ByteString Source #

d_ByteString_426 ∷ a Source #

d_mkByteString_428 ∷ a Source #

d_eqByteString_430 ∷ T_ByteString_426 → T_ByteString_426 → Bool Source #

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

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

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

check__'44'__450 ∷ ∀ xA. ∀ xB. xA → xB → T__'215'__436 xA xB Source #

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

d_proj'8321'_446 ∷ T__'215'__436 AgdaAny AgdaAny → AgdaAny Source #

d_proj'8322'_448 ∷ T__'215'__436 AgdaAny AgdaAny → AgdaAny Source #

d_List_454 ∷ p → () Source #

type T_List_454 a0 = List a0 Source #

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

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

check_'91''93'_458 ∷ ∀ xA. T_List_454 xA Source #

check__'8759'__460 ∷ ∀ xA. xA → T_List_454 xA → T_List_454 xA Source #

cover_List_454 ∷ List a1 → () Source #

d_All_468 ∷ p → p → p → p → () Source #

data T_All_468 Source #

d_length_490 ∷ () → T_List_454 AgdaAny → Integer Source #

du_length_490 ∷ T_List_454 AgdaAny → Integer Source #

d_map_500 ∷ () → () → (AgdaAny → AgdaAny) → T_List_454 AgdaAny → T_List_454 AgdaAny Source #

du_map_500 ∷ (AgdaAny → AgdaAny) → T_List_454 AgdaAny → T_List_454 AgdaAny Source #

d_toList_512 ∷ () → T_List_454 AgdaAny → [AgdaAny] Source #

du_toList_512 ∷ T_List_454 AgdaAny → [AgdaAny] Source #

d_fromList_520 ∷ () → [AgdaAny] → T_List_454 AgdaAny Source #

du_fromList_520 ∷ [AgdaAny] → T_List_454 AgdaAny Source #

d_dropLIST_528 ∷ () → Integer → T_List_454 AgdaAny → T_List_454 AgdaAny Source #

du_dropLIST_528 ∷ Integer → T_List_454 AgdaAny → T_List_454 AgdaAny Source #

d_drop_540 ∷ () → Integer → T_List_454 AgdaAny → () → Integer → T_List_454 AgdaAny → T_List_454 AgdaAny Source #

du_drop_540 ∷ Integer → T_List_454 AgdaAny → T_List_454 AgdaAny Source #

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

d_sequence_580 ∷ () → (() → ()) → T_Monad_254 → T_List_454 AgdaAny → AgdaAny Source #

du_sequence_580 ∷ T_Monad_254 → T_List_454 AgdaAny → AgdaAny Source #

d_mapM_598 ∷ () → () → (() → ()) → T_Monad_254 → (AgdaAny → AgdaAny) → T_List_454 AgdaAny → AgdaAny Source #

du_mapM_598 ∷ T_Monad_254 → (AgdaAny → AgdaAny) → T_List_454 AgdaAny → AgdaAny Source #

type T_Array_602 a0 = Vector a0 Source #

d_Array_602 ∷ a Source #

d_HSlengthOfArray_606 ∷ ∀ xA. () → T_Array_602 xA → Integer Source #

d_HSlistToArray_610 ∷ ∀ xA. () → T_List_454 xA → T_Array_602 xA Source #

d_HSindexArray_612 ∷ ∀ xA. () → T_Array_602 xA → Integer → xA Source #

d_mkArray_616 ∷ a Source #

d_DATA_618 ∷ () Source #

type T_DATA_618 = Data Source #

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

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

pattern C_ListDATA_624 ∷ [Data] → Data Source #

pattern C_iDATA_626 ∷ Integer → Data Source #

pattern C_bDATA_628 ∷ ByteString → Data Source #

check_ConstrDATA_620 ∷ Integer → T_List_454 T_DATA_618 → T_DATA_618 Source #

check_MapDATA_622 ∷ T_List_454 (T__'215'__436 T_DATA_618 T_DATA_618) → T_DATA_618 Source #

check_ListDATA_624 ∷ T_List_454 T_DATA_618 → T_DATA_618 Source #

check_iDATA_626 ∷ Integer → T_DATA_618 Source #

check_bDATA_628 ∷ T_ByteString_426 → T_DATA_618 Source #

cover_DATA_618 ∷ Data → () Source #

d_eqDATA_630 ∷ T_DATA_618 → T_DATA_618 → Bool Source #

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

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

d_eqBls12'45'381'45'G1'45'Element_766 ∷ T_Bls12'45'381'45'G1'45'Element_764 → T_Bls12'45'381'45'G1'45'Element_764 → Bool Source #

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

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

d_eqBls12'45'381'45'G2'45'Element_770 ∷ T_Bls12'45'381'45'G2'45'Element_768 → T_Bls12'45'381'45'G2'45'Element_768 → Bool Source #

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

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

d_eqBls12'45'381'45'MlResult_774 ∷ T_Bls12'45'381'45'MlResult_772 → T_Bls12'45'381'45'MlResult_772 → Bool Source #

d_Kind_776 ∷ () Source #

type T_Kind_776 = KIND Source #

pattern C_'42'_778 ∷ KIND Source #

pattern C_'9839'_780 ∷ KIND Source #

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

check_'42'_778 ∷ T_Kind_776 Source #

check_'9839'_780 ∷ T_Kind_776 Source #

check__'8658'__782 ∷ T_Kind_776 → T_Kind_776 → T_Kind_776 Source #

cover_Kind_776 ∷ KIND → () Source #