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__'215'__364 ∷ p → p → () Source #

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

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

check__'44'__378 ∷ ∀ xA. ∀ xB. xA → xB → T__'215'__364 xA xB Source #

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

d_proj'8321'_374 ∷ T__'215'__364 AgdaAny AgdaAny → AgdaAny Source #

d_proj'8322'_376 ∷ T__'215'__364 AgdaAny AgdaAny → AgdaAny Source #

d_List_382 ∷ p → () Source #

type T_List_382 a0 = List a0 Source #

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

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

check_'91''93'_386 ∷ ∀ xA. T_List_382 xA Source #

check__'8759'__388 ∷ ∀ xA. xA → T_List_382 xA → T_List_382 xA Source #

cover_List_382 ∷ List a1 → () Source #

d_length_392 ∷ () → T_List_382 AgdaAny → Integer Source #

du_length_392 ∷ T_List_382 AgdaAny → Integer Source #

d_map_402 ∷ () → () → (AgdaAny → AgdaAny) → T_List_382 AgdaAny → T_List_382 AgdaAny Source #

du_map_402 ∷ (AgdaAny → AgdaAny) → T_List_382 AgdaAny → T_List_382 AgdaAny Source #

d_toList_414 ∷ () → T_List_382 AgdaAny → [AgdaAny] Source #

du_toList_414 ∷ T_List_382 AgdaAny → [AgdaAny] Source #

d_fromList_422 ∷ () → [AgdaAny] → T_List_382 AgdaAny Source #

du_fromList_422 ∷ [AgdaAny] → T_List_382 AgdaAny Source #

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

d_DATA_450 ∷ () Source #

type T_DATA_450 = Data Source #

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

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

pattern C_ListDATA_456 ∷ [Data] → Data Source #

pattern C_iDATA_458 ∷ Integer → Data Source #

pattern C_bDATA_460 ∷ ByteString → Data Source #

check_ConstrDATA_452 ∷ Integer → T_List_382 T_DATA_450 → T_DATA_450 Source #

check_MapDATA_454 ∷ T_List_382 (T__'215'__364 T_DATA_450 T_DATA_450) → T_DATA_450 Source #

check_ListDATA_456 ∷ T_List_382 T_DATA_450 → T_DATA_450 Source #

check_iDATA_458 ∷ Integer → T_DATA_450 Source #

check_bDATA_460 ∷ T_ByteString_356 → T_DATA_450 Source #

cover_DATA_450 ∷ Data → () Source #

d_eqDATA_462 ∷ T_DATA_450 → T_DATA_450 → Bool Source #

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

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

d_eqBls12'45'381'45'G1'45'Element_466 ∷ T_Bls12'45'381'45'G1'45'Element_464 → T_Bls12'45'381'45'G1'45'Element_464 → Bool Source #

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

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

d_eqBls12'45'381'45'G2'45'Element_470 ∷ T_Bls12'45'381'45'G2'45'Element_468 → T_Bls12'45'381'45'G2'45'Element_468 → Bool Source #

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

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

d_eqBls12'45'381'45'MlResult_474 ∷ T_Bls12'45'381'45'MlResult_472 → T_Bls12'45'381'45'MlResult_472 → Bool Source #

d_Kind_476 ∷ () Source #

type T_Kind_476 = KIND Source #

pattern C_'42'_478 ∷ KIND Source #

pattern C_'9839'_480 ∷ KIND Source #

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

check_'42'_478 ∷ T_Kind_476 Source #

check_'9839'_480 ∷ T_Kind_476 Source #

check__'8658'__482 ∷ T_Kind_476 → T_Kind_476 → T_Kind_476 Source #

cover_Kind_476 ∷ KIND → () Source #