Documentation

type T_Term_14 = DefaultFun () #

d_TermU_24 :: a #

d_parseTm_26 :: T_String_6 -> T_Either_6 T_ParseError_4 T_TermN_18 #

d_parseTmU_28 :: T_String_6 -> T_Either_6 T_ParseError_4 T_TermNU_22 #

d_parseTy_30 :: T_String_6 -> T_Either_6 T_ParseError_4 T_TypeN_20 #

d_deBruijnifyTm_32 :: T_TermN_18 -> T_Either_6 T_FreeVariableError_574 T_Term_14 #

d_deBruijnifyTy_34 :: T_TypeN_20 -> T_Either_6 T_FreeVariableError_574 T_Type_16 #

d_deBruijnifyTmU_36 :: T_TermNU_22 -> T_Either_6 T_FreeVariableError_574 T_TermU_24 #

d_convTm_38 :: T_Term_14 -> T_RawTm_32 #

d_unconvTm_40 :: T_RawTm_32 -> T_Term_14 #

d_convTy_42 :: T_Type_16 -> T_RawTy_2 #

d_unconvTy_44 :: T_RawTy_2 -> T_Type_16 #

d_convTmU_46 :: T_TermU_24 -> T_Untyped_208 #

d_unconvTmU_48 :: T_Untyped_208 -> T_TermU_24 #

checkKindAgda :: T_Type_16 -> T_Kind_766 -> T_Either_6 T_ERROR_12 T_'8868'_6 #

d_checkKindX_50 :: T_Type_16 -> T_Kind_766 -> T_Either_6 T_ERROR_12 T_'8868'_6 #

inferKindAgda :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_766 #

d_inferKind'8709'_68 :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_766 #

normalizeTypeAgda :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16 #

d_normalizeType_80 :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16 #

inferTypeAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16 #

d_inferType'8709'_92 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16 #

checkTypeAgda :: T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 T_'8868'_6 #

d_checkType'8709'_104 :: T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 T_'8868'_6 #

normalizeTypeTermAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14 #

d_normalizeTypeTerm_120 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14 #

runTLAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14 #

d_runTL_132 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14 #

runTCKAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14 #

d_runTCK_146 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14 #

runTCEKAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14 #

d_runTCEK_166 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14 #

d_runUValue_186 :: T__'8866'_14 -> T_Either_6 T_ERROR_12 T_Value_14 #

runUAgda :: T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24 #

d_runU_194 :: T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24 #

runUCountingAgda :: T__'215'__426 T_HCekMachineCosts_4 (T_List_444 (T__'215'__426 T_String_6 T_CpuAndMemoryModel_192)) -> T_TermU_24 -> T_Either_6 T_ERROR_12 (T__'215'__426 T_TermU_24 (T__'215'__426 Integer Integer)) #

d_runUCounting_202 :: T__'215'__426 T_HCekMachineCosts_4 (T_List_444 (T__'215'__426 T_String_6 T_CpuAndMemoryModel_192)) -> T_TermU_24 -> T_Either_6 T_ERROR_12 (T__'215'__426 T_TermU_24 (T__'215'__426 Integer Integer)) #

blah :: T_String_6 -> T_String_6 -> T_String_6 #

d_blah_240 :: T_String_6 -> T_String_6 -> T_String_6 #

printTy :: T_String_6 -> T_String_6 #

d_printTy_286 :: T_String_6 -> T_String_6 #

alphaTy :: T_String_6 -> T_String_6 -> Bool #

d_alphaTy_314 :: T_String_6 -> T_String_6 -> Bool #

alphaTm :: T_String_6 -> T_String_6 -> Bool #

d_alphaTm_360 :: T_String_6 -> T_String_6 -> Bool #

alphaU :: T_String_6 -> T_String_6 -> Bool #

d_alphaU_406 :: T_String_6 -> T_String_6 -> Bool #