Documentation

type Tag = DefaultUni Source #

pattern TagInt ∷ () ⇒ a ~ Esc Integer ⇒ DefaultUni a Source #

pattern TagBS ∷ () ⇒ a ~ Esc ByteString ⇒ DefaultUni a Source #

pattern TagStr ∷ () ⇒ a ~ Esc Text ⇒ DefaultUni a Source #

pattern TagBool ∷ () ⇒ a ~ Esc Bool ⇒ DefaultUni a Source #

pattern TagUnit ∷ () ⇒ a ~ Esc () ⇒ DefaultUni a Source #

pattern TagData ∷ () ⇒ a ~ Esc Data ⇒ DefaultUni a Source #

pattern TagPair ∷ ∀ {a} {k1} {k2} {f1 ∷ k1 → k2} {a1 ∷ k1} {k3} {k4} {f2 ∷ k3 → k4} {a2 ∷ k3}. () ⇒ ∀. (a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) ⇒ DefaultUni (Esc a2) → DefaultUni (Esc a1) → DefaultUni a Source #

pattern TagList ∷ ∀ {a} {k1} {k2} {f ∷ k1 → k2} {a1 ∷ k1}. () ⇒ ∀. (a ~ Esc (f a1), Esc f ~ Esc List) ⇒ DefaultUni (Esc a1) → DefaultUni a Source #

pattern TagArray ∷ ∀ {a} {k1} {k2} {f ∷ k1 → k2} {a1 ∷ k1}. () ⇒ ∀. (a ~ Esc (f a1), Esc f ~ Esc Vector) ⇒ DefaultUni (Esc a1) → DefaultUni a Source #

pattern TagBLS12_381_G1_Element ∷ () ⇒ a ~ Esc Element ⇒ DefaultUni a Source #

pattern TagBLS12_381_G2_Element ∷ () ⇒ a ~ Esc Element ⇒ DefaultUni a Source #

pattern TagBLS12_381_MlResult ∷ () ⇒ a ~ Esc MlResult ⇒ DefaultUni a Source #

type TagCon = Some (ValueOf DefaultUni) Source #

pattern TagCon ∷ () ⇒ uni (Esc a) → a → Some (ValueOf uni) Source #

d_SigTy_4 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

d_convSigTy_6 ∷ Integer → Integer → Integer → T__'8724'_'8803'__120 → T__'8724'_'8803'__120 → Integer → Integer → Integer → T__'8724'_'8803'__120 → T__'8724'_'8803'__120 → Integer → Integer → T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 → T__'8801'__12 → T_SigTy_266 → T_SigTy_266 Source #

du_convSigTy_6 ∷ T_SigTy_266 → T_SigTy_266 Source #

d_sig2type_8 ∷ T_Sig_72 → T__'8866'Nf'8902'__4 Source #

d_sigTy2type_10 ∷ T_Ctx'8902'_2 → Integer → Integer → Integer → Integer → Integer → Integer → T__'8866'Nf'8902'__4 → T__'8724'_'8803'__120 → T__'8724'_'8803'__120 → T_SigTy_266 → T__'8866'Nf'8902'__4 Source #

du_sigTy2type_10 ∷ T__'8866'Nf'8902'__4 → T__'8866'Nf'8902'__4 Source #

d_'8866''9839'2TyNe'9839'_12 ∷ Integer → Integer → T__'8866''9839'_4 → T__'8866'Ne'8902'__6 Source #

d_Esc_24 ∷ p → () Source #

type T_Esc_24 a0 = Esc a0 Source #

cover_Esc_24 ∷ Esc a1 → () Source #

d_Tag_28 ∷ p → () Source #

type T_Tag_28 = Tag Source #

pattern C_integer_30 ∷ () ⇒ a ~ Esc Integer ⇒ DefaultUni a Source #

pattern C_bytestring_32 ∷ () ⇒ a ~ Esc ByteString ⇒ DefaultUni a Source #

pattern C_string_34 ∷ () ⇒ a ~ Esc Text ⇒ DefaultUni a Source #

pattern C_bool_36 ∷ () ⇒ a ~ Esc Bool ⇒ DefaultUni a Source #

pattern C_unit_38 ∷ () ⇒ a ~ Esc () ⇒ DefaultUni a Source #

pattern C_pdata_40 ∷ () ⇒ a ~ Esc Data ⇒ DefaultUni a Source #

pattern C_pair_46 ∷ ∀ {a} {k1} {k2} {f1 ∷ k1 → k2} {a1 ∷ k1} {k3} {k4} {f2 ∷ k3 → k4} {a2 ∷ k3}. () ⇒ ∀. (a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) ⇒ DefaultUni (Esc a2) → DefaultUni (Esc a1) → DefaultUni a Source #

pattern C_list_50 ∷ ∀ {a} {k1} {k2} {f ∷ k1 → k2} {a1 ∷ k1}. () ⇒ ∀. (a ~ Esc (f a1), Esc f ~ Esc List) ⇒ DefaultUni (Esc a1) → DefaultUni a Source #

pattern C_array_54 ∷ ∀ {a} {k1} {k2} {f ∷ k1 → k2} {a1 ∷ k1}. () ⇒ ∀. (a ~ Esc (f a1), Esc f ~ Esc Vector) ⇒ DefaultUni (Esc a1) → DefaultUni a Source #

pattern C_bls12'45'381'45'g1'45'element_56 ∷ () ⇒ a ~ Esc Element ⇒ DefaultUni a Source #

pattern C_bls12'45'381'45'g2'45'element_58 ∷ () ⇒ a ~ Esc Element ⇒ DefaultUni a Source #

pattern C_bls12'45'381'45'mlresult_60 ∷ () ⇒ a ~ Esc MlResult ⇒ DefaultUni a Source #

check_integer_30 ∷ T_Tag_28 (T_Esc_24 Integer) Source #

check_bytestring_32 ∷ T_Tag_28 (T_Esc_24 T_ByteString_356) Source #

check_string_34 ∷ T_Tag_28 (T_Esc_24 T_String_6) Source #

check_bool_36 ∷ T_Tag_28 (T_Esc_24 Bool) Source #

check_unit_38 ∷ T_Tag_28 (T_Esc_24 T_'8868'_6) Source #

check_pdata_40 ∷ T_Tag_28 (T_Esc_24 T_DATA_494) Source #

check_pair_46 ∷ ∀ xA. ∀ xB. T_Tag_28 (T_Esc_24 xA) → T_Tag_28 (T_Esc_24 xB) → T_Tag_28 (T_Esc_24 (T__'215'__366 xA xB)) Source #

check_list_50 ∷ ∀ xA. T_Tag_28 (T_Esc_24 xA) → T_Tag_28 (T_Esc_24 (T_List_384 xA)) Source #

check_array_54 ∷ ∀ xA. T_Tag_28 (T_Esc_24 xA) → T_Tag_28 (T_Esc_24 (T_Array_478 xA)) Source #

check_bls12'45'381'45'g1'45'element_56 ∷ T_Tag_28 (T_Esc_24 T_Bls12'45'381'45'G1'45'Element_640) Source #

check_bls12'45'381'45'g2'45'element_58 ∷ T_Tag_28 (T_Esc_24 T_Bls12'45'381'45'G2'45'Element_644) Source #

check_bls12'45'381'45'mlresult_60 ∷ T_Tag_28 (T_Esc_24 T_Bls12'45'381'45'MlResult_648) Source #

cover_Tag_28 ∷ Tag a1 → () Source #

d_TyTag_62 ∷ () Source #

d_'10214'_'10215'tag_64 ∷ T__'8866''9839'_4 → () Source #

d_decTyTag_68 ∷ T__'8866''9839'_4 → T__'8866''9839'_4 → T_Dec_20 Source #

d_TagCon_106 ∷ () Source #

type T_TagCon_106 = TagCon Source #

pattern C_tagCon_110 ∷ () ⇒ uni (Esc a) → a → Some (ValueOf uni) Source #

check_tagCon_110 ∷ ∀ xA. T_Tag_28 (T_Esc_24 xA) → xA → T_TagCon_106 Source #

cover_TagCon_106 ∷ TagCon → () Source #

d_decTagCon''_124 ∷ () → () → T_Tag_28 (T_Esc_24 AgdaAny) → AgdaAny → T_Tag_28 (T_Esc_24 AgdaAny) → AgdaAny → Bool Source #

du_decTagCon''_124 ∷ T_Tag_28 (T_Esc_24 AgdaAny) → AgdaAny → T_Tag_28 (T_Esc_24 AgdaAny) → AgdaAny → Bool Source #

d_decTagCon_192 ∷ T_TagCon_106 → T_TagCon_106 → Bool Source #

d_TmCon_202 ∷ () Source #

data T_TmCon_202 Source #

d_Untyped_208 ∷ () Source #

type T_Untyped_208 = UTerm Source #

pattern C_UVar_210 ∷ Integer → UTerm Source #

pattern C_ULambda_212 ∷ UTerm → UTerm Source #

pattern C_UApp_214 ∷ UTerm → UTerm → UTerm Source #

pattern C_UCon_216 ∷ Some (ValueOf DefaultUni) → UTerm Source #

pattern C_UError_218 ∷ UTerm Source #

pattern C_UBuiltin_220 ∷ DefaultFun → UTerm Source #

pattern C_UDelay_222 ∷ UTerm → UTerm Source #

pattern C_UForce_224 ∷ UTerm → UTerm Source #

pattern C_UConstr_226 ∷ Integer → [UTerm] → UTerm Source #

pattern C_UCase_228 ∷ UTerm → [UTerm] → UTerm Source #

check_UVar_210 ∷ Integer → T_Untyped_208 Source #

check_ULambda_212 ∷ T_Untyped_208 → T_Untyped_208 Source #

check_UApp_214 ∷ T_Untyped_208 → T_Untyped_208 → T_Untyped_208 Source #

check_UCon_216 ∷ T_TagCon_106 → T_Untyped_208 Source #

check_UError_218 ∷ T_Untyped_208 Source #

check_UBuiltin_220 ∷ T_Builtin_2 → T_Untyped_208 Source #

check_UDelay_222 ∷ T_Untyped_208 → T_Untyped_208 Source #

check_UForce_224 ∷ T_Untyped_208 → T_Untyped_208 Source #

check_UConstr_226 ∷ Integer → T_List_384 T_Untyped_208 → T_Untyped_208 Source #

check_UCase_228 ∷ T_Untyped_208 → T_List_384 T_Untyped_208 → T_Untyped_208 Source #

cover_Untyped_208 ∷ UTerm → () Source #

d_tag2TyTag_232 ∷ () → T_Tag_28 AgdaAny → T__'8866''9839'_4 Source #

du_tag2TyTag_232 ∷ T_Tag_28 AgdaAny → T__'8866''9839'_4 Source #

d_tagLemma_246 ∷ () → T_Tag_28 (T_Esc_24 AgdaAny) → T__'8801'__12 Source #

d_tagCon2TmCon_256 ∷ T_TagCon_106 → T_TmCon_202 Source #

d_tyTag2Tag_310 ∷ T__'8866''9839'_4 → T_Σ_14 Source #

d_tyTagLemma_358 ∷ T__'8866''9839'_4 → T__'8801'__12 Source #

d_tmCon2TagCon_368 ∷ T_TmCon_202 → T_TagCon_106 Source #