Documentation

type T_Term_14 = Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun () Source #

d_Term_14 ∷ a Source #

type T_Type_16 = Type NamedTyDeBruijn DefaultUni () Source #

d_Type_16 ∷ a Source #

type T_TermN_18 = Term TyName Name DefaultUni DefaultFun SrcSpan Source #

d_TermN_18 ∷ a Source #

type T_TypeN_20 = Type TyName DefaultUni SrcSpan Source #

d_TypeN_20 ∷ a Source #

type T_TermNU_22 = Term Name DefaultUni DefaultFun SrcSpan Source #

d_TermNU_22 ∷ a Source #

type T_TermU_24 = Term NamedDeBruijn DefaultUni DefaultFun () Source #

d_TermU_24 ∷ a Source #

d_parseTm_26 ∷ T_String_6 → T_Either_6 T_ParseError_4 T_TermN_18 Source #

d_parseTmU_28 ∷ T_String_6 → T_Either_6 T_ParseError_4 T_TermNU_22 Source #

d_parseTy_30 ∷ T_String_6 → T_Either_6 T_ParseError_4 T_TypeN_20 Source #

d_deBruijnifyTm_32 ∷ T_TermN_18 → T_Either_6 T_FreeVariableError_574 T_Term_14 Source #

d_deBruijnifyTy_34 ∷ T_TypeN_20 → T_Either_6 T_FreeVariableError_574 T_Type_16 Source #

d_deBruijnifyTmU_36 ∷ T_TermNU_22 → T_Either_6 T_FreeVariableError_574 T_TermU_24 Source #

d_convTm_38 ∷ T_Term_14 → T_RawTm_30 Source #

d_unconvTm_40 ∷ T_RawTm_30 → T_Term_14 Source #

d_convTy_42 ∷ T_Type_16 → T_RawTy_2 Source #

d_unconvTy_44 ∷ T_RawTy_2 → T_Type_16 Source #

d_convTmU_46 ∷ T_TermU_24 → T_Untyped_146 Source #

d_unconvTmU_48 ∷ T_Untyped_146 → T_TermU_24 Source #

checkKindAgda ∷ T_Type_16 → T_Kind_476 → T_Either_6 T_ERROR_12 T_'8868'_6 Source #

d_checkKindX_50 ∷ T_Type_16 → T_Kind_476 → T_Either_6 T_ERROR_12 T_'8868'_6 Source #

inferKindAgda ∷ T_Type_16 → T_Either_6 T_ERROR_12 T_Kind_476 Source #

d_inferKind'8709'_68 ∷ T_Type_16 → T_Either_6 T_ERROR_12 T_Kind_476 Source #

normalizeTypeAgda ∷ T_Type_16 → T_Either_6 T_ERROR_12 T_Type_16 Source #

d_normalizeType_80 ∷ T_Type_16 → T_Either_6 T_ERROR_12 T_Type_16 Source #

inferTypeAgda ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Type_16 Source #

d_inferType'8709'_92 ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Type_16 Source #

checkTypeAgda ∷ T_Type_16 → T_Term_14 → T_Either_6 T_ERROR_12 T_'8868'_6 Source #

d_checkType'8709'_104 ∷ T_Type_16 → T_Term_14 → T_Either_6 T_ERROR_12 T_'8868'_6 Source #

normalizeTypeTermAgda ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Term_14 Source #

d_normalizeTypeTerm_120 ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Term_14 Source #

runTLAgda ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Term_14 Source #

d_runTL_132 ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Term_14 Source #

runTCKAgda ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Term_14 Source #

d_runTCK_146 ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Term_14 Source #

runTCEKAgda ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Term_14 Source #

d_runTCEK_166 ∷ T_Term_14 → T_Either_6 T_ERROR_12 T_Term_14 Source #

d_runUValue_186 ∷ T__'8866'_14 → T_Either_6 T_ERROR_12 T_Value_14 Source #

runUAgda ∷ T_TermU_24 → T_Either_6 T_ERROR_12 T_TermU_24 Source #

d_runU_194 ∷ T_TermU_24 → T_Either_6 T_ERROR_12 T_TermU_24 Source #

runUCountingAgda ∷ T__'215'__364 T_HCekMachineCosts_4 (T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)) → T_TermU_24 → T_Either_6 T_ERROR_12 (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer)) Source #

d_runUCounting_202 ∷ T__'215'__364 T_HCekMachineCosts_4 (T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)) → T_TermU_24 → T_Either_6 T_ERROR_12 (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer)) Source #

blah ∷ T_String_6 → T_String_6 → T_String_6 Source #

d_blah_240 ∷ T_String_6 → T_String_6 → T_String_6 Source #

printTy ∷ T_String_6 → T_String_6 Source #

d_printTy_286 ∷ T_String_6 → T_String_6 Source #

alphaTy ∷ T_String_6 → T_String_6 → Bool Source #

d_alphaTy_314 ∷ T_String_6 → T_String_6 → Bool Source #

alphaTm ∷ T_String_6 → T_String_6 → Bool Source #

d_alphaTm_360 ∷ T_String_6 → T_String_6 → Bool Source #

alphaU ∷ T_String_6 → T_String_6 → Bool Source #

d_alphaU_406 ∷ T_String_6 → T_String_6 → Bool Source #