| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algorithmic.Erasure
Documentation
d_len'8902'_4 :: T_Ctx'8902'_2 -> Integer #
d_len_12 :: T_Ctx'8902'_2 -> T_Ctx_2 -> Integer #
d_eraseVar_28 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8715'__16 -> T_Fin_10 #
du_eraseVar_28 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_Fin_10 #
d_eraseTC_36 :: T__'8866'Nf'8902'__4 -> AgdaAny -> T_TmCon_202 #
d_erase_48 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8866'__178 -> T__'8866'_14 #
d_erase'45'ConstrArgs_58 :: T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> T_IList_302 -> [T__'8866'_14] #
d_erase'45'Cases_76 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> Integer -> T_Vec_28 -> T_Cases_172 -> [T__'8866'_14] #
du_erase'45'Cases_76 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T_Vec_28 -> T_Cases_172 -> [T__'8866'_14] #
d_lenLemma_130 :: T_Ctx'8902'_2 -> T_Ctx_16 -> T__'8801'__12 #
d_lemzero_154 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #
d_lemsuc_166 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T_Fin_10 -> T__'8801'__12 #
d_lem'8801'Ctx_176 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T_Ctx_2 -> T__'8801'__12 -> T__'8801'__12 #
d_lem'45'conv'8715'_194 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4 -> T__'8801'__12 -> T__'8801'__12 -> T__'8715'__16 -> T__'8801'__12 #
d_sameVar_206 :: T_Ctx'8902'_2 -> T_Ctx_16 -> T__'8866''8902'__20 -> T__'8715'__34 -> T__'8801'__12 #
d_lemVar_228 :: Integer -> Integer -> T__'8801'__12 -> T_Fin_10 -> T__'8801'__12 #
d_lemƛ_242 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8866'_14 -> T__'8801'__12 #
d_lem'183'_256 :: Integer -> Integer -> T__'8801'__12 -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 #
d_lem'45'delay_270 :: Integer -> Integer -> T__'8801'__12 -> T__'8866'_14 -> T__'8801'__12 #
d_lem'45'force_282 :: Integer -> Integer -> T__'8801'__12 -> T__'8866'_14 -> T__'8801'__12 #
d_lemcon''_294 :: Integer -> Integer -> T__'8801'__12 -> T_TmCon_202 -> T__'8801'__12 #
d_lemerror_304 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #
d_lembuiltin_314 :: Integer -> Integer -> T_Builtin_2 -> T__'8801'__12 -> T__'8801'__12 #
d_lemConstr_328 :: Integer -> Integer -> Integer -> [T__'8866'_14] -> T__'8801'__12 -> T__'8801'__12 #
d_lemCase_350 :: Integer -> Integer -> T__'8866'_14 -> [T__'8866'_14] -> T__'8801'__12 -> T__'8801'__12 #
d_lem'45'erase_372 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4 -> T__'8801'__12 -> T__'8801'__12 -> T__'8866'__178 -> T__'8801'__12 #
d_lem'45'subst_382 :: Integer -> T__'8866'_14 -> T__'8801'__12 -> T__'8801'__12 #
d_lem'45'erase''_398 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4 -> T__'8801'__12 -> T__'8866'__178 -> T__'8801'__12 #
d_lem'45'erase''''_420 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4 -> T__'8801'__12 -> T__'8866'__178 -> T__'8801'__12 #
d_same_432 :: T_Ctx'8902'_2 -> T_Ctx_16 -> T__'8866''8902'__20 -> T__'8866'__110 -> T__'8801'__12 #
d_'43'cancel_442 :: Integer -> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #
d_same'45'ConstrArgs_454 :: T_Ctx'8902'_2 -> T_Ctx_16 -> [T__'8866''8902'__20] -> T_IList_302 -> T__'8801'__12 #
d_same'45'mkCaseType_478 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4 -> T__'8866'__178 -> T__'8801'__12 -> T__'8801'__12 #
d_same'45'Cases_494 :: T_Ctx'8902'_2 -> T_Ctx_16 -> T__'8866''8902'__20 -> Integer -> T_Vec_28 -> T_Cases_104 -> T__'8801'__12 #
d_same''Len_596 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8801'__12 #
d_lem'45'Dconv'8715'_622 :: T_Ctx'8902'_2 -> T_Ctx_16 -> T_Ctx_16 -> T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8801'__12 -> T__'8801'__12 -> T__'8715'__34 -> T__'8801'__12 #
d_same''Var_634 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8715'__16 -> T__'8801'__12 #
d_same''TC_656 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> AgdaAny -> T__'8801'__12 #
d_same''_674 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T__'8866'__178 -> T__'8801'__12 #
d_same''ConstrArgs_684 :: T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> T_IList_302 -> T__'8801'__12 #
d_same'45'subst_702 :: T_Ctx'8902'_2 -> T_Ctx_16 -> T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866'__110 -> T__'8801'__12 -> T__'8801'__12 #
d_same''Case_718 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> Integer -> T_Vec_28 -> T_Cases_172 -> T__'8801'__12 #