| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Type.BetaNBE.Completeness
Documentation
d_CR_10 :: T_Ctx'8902'_2 -> T_Kind_766 -> AgdaAny -> AgdaAny -> () #
d_Unif_64 :: T_Ctx'8902'_2 -> T_Kind_766 -> T_Kind_766 -> (T_Ctx'8902'_2 -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny -> AgdaAny) -> (T_Ctx'8902'_2 -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny -> AgdaAny) -> T_Ctx'8902'_2 -> T_Kind_766 -> T_Kind_766 -> (T_Ctx'8902'_2 -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny -> AgdaAny) -> () #
d_symCR_100 :: T_Ctx'8902'_2 -> T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_symCR_100 :: T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_transCR_158 :: T_Ctx'8902'_2 -> T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_transCR_158 :: T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_reflCR_256 :: T_Ctx'8902'_2 -> T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_reflCR_256 :: T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_reflectCR_266 :: T_Ctx'8902'_2 -> T_Kind_766 -> T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6 -> T__'8801'__12 -> AgdaAny #
du_reflectCR_266 :: T_Kind_766 -> T__'8801'__12 -> AgdaAny #
d_reifyCR_284 :: T_Ctx'8902'_2 -> T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 #
d_EnvCR_338 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> () #
d_CR'44''44''8902'_356 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny #
du_CR'44''44''8902'_356 :: (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny -> T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny #
d_AppCR_376 :: T_Ctx'8902'_2 -> T_Kind_766 -> T_Kind_766 -> T__'8846'__30 -> T__'8846'__30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_AppCR_376 :: T_Ctx'8902'_2 -> T_Kind_766 -> T__'8846'__30 -> T__'8846'__30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_renVal'45'reflect_416 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> T__'8866'Ne'8902'__6 -> AgdaAny #
d_ren'45'reify_444 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> T__'8801'__12 #
d_renVal'45'id_524 :: T_Ctx'8902'_2 -> T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_renVal'45'id_524 :: T_Kind_766 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_renVal'45'comp_576 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_renVal'45'comp_576 :: T_Kind_766 -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_renCR_670 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> AgdaAny -> AgdaAny -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny -> AgdaAny #
du_renCR_670 :: T_Kind_766 -> AgdaAny -> AgdaAny -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny -> AgdaAny #
d_renVal'183'V_754 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> T_Kind_766 -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> T__'8846'__30 -> T__'8846'__30 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_idext_840 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> T__'8866''8902'__20 -> AgdaAny #
d_idext'45'List_848 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> [T__'8866''8902'__20] -> T__'8801'__12 #
d_idext'45'VecList_858 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> Integer -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> T_Vec_28 -> T__'8801'__12 #
d_renVal'45'eval_878 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> T__'8866''8902'__20 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny #
d_renVal'45'eval'45'List_896 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> [T__'8866''8902'__20] -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> T__'8801'__12 #
d_renVal'45'eval'45'VecList_916 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> Integer -> T_Vec_28 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> T__'8801'__12 #
d_ren'45'eval_1144 :: T_Ctx'8902'_2 -> T_Kind_766 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T__'8866''8902'__20 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny #
d_ren'45'eval'45'List_1158 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> [T__'8866''8902'__20] -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> T__'8801'__12 #
d_ren'45'eval'45'VecList_1174 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> Integer -> T_Vec_28 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8715''8902'__14) -> T__'8801'__12 #
d_sub'45'eval_1314 :: T_Ctx'8902'_2 -> T_Kind_766 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T__'8866''8902'__20 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8866''8902'__20) -> AgdaAny #
d_sub'45'eval'45'List_1330 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> [T__'8866''8902'__20] -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8866''8902'__20) -> T__'8801'__12 #
d_sub'45'eval'45'VecList_1348 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> Integer -> T_Vec_28 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> T__'8866''8902'__20) -> T__'8801'__12 #
d_fund_1482 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> T_Kind_766 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8801'β__10 -> AgdaAny #
d_fund'45'List_1492 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> [T__'8866''8902'__20] -> [T__'8866''8902'__20] -> T__'91''8801''93'β__4 -> T__'8801'__12 #
d_fund'45'VecList_1504 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> Integer -> (T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny) -> T_Vec_28 -> T_Vec_28 -> T__'10216''91''8801''93''10217'β__8 -> T__'8801'__12 #
d_idCR_1618 :: T_Ctx'8902'_2 -> T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny #
du_idCR_1618 :: T_Kind_766 -> AgdaAny #
d_completeness_1626 :: T_Ctx'8902'_2 -> T_Kind_766 -> T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8801'β__10 -> T__'8801'__12 #
d_exte'45'lem_1634 :: T_Ctx'8902'_2 -> T_Kind_766 -> T_Kind_766 -> T__'8715''8902'__14 -> AgdaAny #