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 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_260 → T_SigTy_260 Source #

du_convSigTy_6 ∷ T_SigTy_260 → T_SigTy_260 Source #

d_sig2type_8 ∷ T_Sig_68 → 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_260 → 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_bls12'45'381'45'g1'45'element_52 ∷ () ⇒ a ~ Esc Element ⇒ DefaultUni a Source #

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

pattern C_bls12'45'381'45'mlresult_56 ∷ () ⇒ 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_450) 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'__364 xA xB)) Source #

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

check_bls12'45'381'45'g1'45'element_52 ∷ T_Tag_28 (T_Esc_24 T_Bls12'45'381'45'G1'45'Element_464) Source #

check_bls12'45'381'45'g2'45'element_54 ∷ T_Tag_28 (T_Esc_24 T_Bls12'45'381'45'G2'45'Element_468) Source #

check_bls12'45'381'45'mlresult_56 ∷ T_Tag_28 (T_Esc_24 T_Bls12'45'381'45'MlResult_472) Source #

cover_Tag_28 ∷ Tag a1 → () Source #

d_TagCon_58 ∷ () Source #

type T_TagCon_58 = TagCon Source #

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

check_tagCon_62 ∷ ∀ xA. T_Tag_28 (T_Esc_24 xA) → xA → T_TagCon_58 Source #

cover_TagCon_58 ∷ TagCon → () Source #

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

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

d_decTagCon_136 ∷ T_TagCon_58 → T_TagCon_58 → Bool Source #

d_Untyped_146 ∷ () Source #

type T_Untyped_146 = UTerm Source #

pattern C_UVar_148 ∷ Integer → UTerm Source #

pattern C_ULambda_150 ∷ UTerm → UTerm Source #

pattern C_UApp_152 ∷ UTerm → UTerm → UTerm Source #

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

pattern C_UError_156 ∷ UTerm Source #

pattern C_UBuiltin_158 ∷ DefaultFun → UTerm Source #

pattern C_UDelay_160 ∷ UTerm → UTerm Source #

pattern C_UForce_162 ∷ UTerm → UTerm Source #

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

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

check_UVar_148 ∷ Integer → T_Untyped_146 Source #

check_ULambda_150 ∷ T_Untyped_146 → T_Untyped_146 Source #

check_UApp_152 ∷ T_Untyped_146 → T_Untyped_146 → T_Untyped_146 Source #

check_UCon_154 ∷ T_TagCon_58 → T_Untyped_146 Source #

check_UError_156 ∷ T_Untyped_146 Source #

check_UBuiltin_158 ∷ T_Builtin_2 → T_Untyped_146 Source #

check_UDelay_160 ∷ T_Untyped_146 → T_Untyped_146 Source #

check_UForce_162 ∷ T_Untyped_146 → T_Untyped_146 Source #

check_UConstr_164 ∷ Integer → T_List_382 T_Untyped_146 → T_Untyped_146 Source #

check_UCase_166 ∷ T_Untyped_146 → T_List_382 T_Untyped_146 → T_Untyped_146 Source #

cover_Untyped_146 ∷ UTerm → () Source #

d_TyTag_168 ∷ () Source #

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

d_decTag_174 ∷ T__'8866''9839'_4 → T__'8866''9839'_4 → T_Dec_32 Source #

d_TmCon_198 ∷ () Source #

data T_TmCon_198 Source #

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

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

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

d_tagCon2TmCon_226 ∷ T_TagCon_58 → T_TmCon_198 Source #

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

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

d_tmCon2TagCon_316 ∷ T_TmCon_198 → T_TagCon_58 Source #