| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Type.BetaNBE.Completeness
Documentation
d_CR_10 ∷ T_Ctx'8902'_2 → T_Kind_476 → AgdaAny → AgdaAny → () Source #
d_Unif_64 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → (T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny → AgdaAny) → (T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny → AgdaAny) → T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → (T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny → AgdaAny) → () Source #
d_symCR_100 ∷ T_Ctx'8902'_2 → T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_symCR_100 ∷ T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_transCR_158 ∷ T_Ctx'8902'_2 → T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_transCR_158 ∷ T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_reflCR_256 ∷ T_Ctx'8902'_2 → T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_reflCR_256 ∷ T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_reflectCR_266 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866'Ne'8902'__6 → T__'8866'Ne'8902'__6 → T__'8801'__12 → AgdaAny Source #
d_reifyCR_284 ∷ T_Ctx'8902'_2 → T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 Source #
d_EnvCR_338 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → () Source #
d_CR'44''44''8902'_356 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Kind_476 → T__'8715''8902'__14 → AgdaAny Source #
du_CR'44''44''8902'_356 ∷ (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → AgdaAny → T_Kind_476 → T__'8715''8902'__14 → AgdaAny Source #
d_AppCR_376 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → T__'8846'__30 → T__'8846'__30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_AppCR_376 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8846'__30 → T__'8846'__30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_renVal'45'reflect_416 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8866'Ne'8902'__6 → AgdaAny Source #
d_ren'45'reify_444 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8801'__12 Source #
d_renVal'45'id_524 ∷ T_Ctx'8902'_2 → T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_renVal'45'id_524 ∷ T_Kind_476 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_renVal'45'comp_576 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_renVal'45'comp_576 ∷ T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_renCR_670 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → AgdaAny → AgdaAny → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny → AgdaAny Source #
du_renCR_670 ∷ T_Kind_476 → AgdaAny → AgdaAny → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny → AgdaAny Source #
d_renVal'183'V_754 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8846'__30 → T__'8846'__30 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_idext_840 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T__'8866''8902'__20 → AgdaAny Source #
d_idext'45'List_848 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → [T__'8866''8902'__20] → T__'8801'__12 Source #
d_idext'45'VecList_858 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → Integer → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T_Vec_28 → T__'8801'__12 Source #
d_renVal'45'eval_878 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → T__'8866''8902'__20 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny Source #
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_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8801'__12 Source #
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_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8801'__12 Source #
d_ren'45'eval_1144 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Ctx'8902'_2 → T_Ctx'8902'_2 → T__'8866''8902'__20 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → AgdaAny Source #
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_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8801'__12 Source #
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_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T__'8801'__12 Source #
d_sub'45'eval_1314 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Ctx'8902'_2 → T_Ctx'8902'_2 → T__'8866''8902'__20 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → AgdaAny Source #
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_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → T__'8801'__12 Source #
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_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → T__'8801'__12 Source #
d_fund_1482 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T__'8866''8902'__20 → T__'8866''8902'__20 → T__'8801'β__10 → AgdaAny Source #
d_fund'45'List_1492 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → [T__'8866''8902'__20] → [T__'8866''8902'__20] → T__'91''8801''93'β__4 → T__'8801'__12 Source #
d_fund'45'VecList_1504 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → Integer → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T_Vec_28 → T_Vec_28 → T__'10216''91''8801''93''10217'β__8 → T__'8801'__12 Source #