| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Type.BetaNBE.Soundness
Documentation
d_SR_10 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866''8902'__20 → AgdaAny → () Source #
d_reflectSR_54 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866''8902'__20 → T__'8866'Ne'8902'__6 → T__'8801'β__10 → AgdaAny Source #
d_reifySR_74 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866''8902'__20 → AgdaAny → AgdaAny → T__'8801'β__10 Source #
d_SREnv_108 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → () Source #
d_SR'44''44''8902'_134 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T_Kind_476 → T__'8866''8902'__20 → AgdaAny → AgdaAny → T_Kind_476 → T__'8715''8902'__14 → AgdaAny Source #
du_SR'44''44''8902'_134 ∷ (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → AgdaAny → T_Kind_476 → T__'8715''8902'__14 → AgdaAny Source #
d_subSR_156 ∷ T_Ctx'8902'_2 → T_Kind_476 → T__'8866''8902'__20 → T__'8866''8902'__20 → T__'8801'β__10 → AgdaAny → AgdaAny → AgdaAny Source #
du_subSR_156 ∷ T_Kind_476 → T__'8866''8902'__20 → T__'8801'β__10 → AgdaAny → AgdaAny → AgdaAny Source #
d_renSR_202 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8715''8902'__14) → T_Kind_476 → T__'8866''8902'__20 → AgdaAny → AgdaAny → AgdaAny Source #
d_exts'45'sub'45'cons_268 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → T__'8715''8902'__14 → T__'8801'__12 Source #
d_subSREnv_288 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → T__'8801'__12) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T_Kind_476 → T__'8715''8902'__14 → AgdaAny Source #
du_subSREnv_288 ∷ (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T_Kind_476 → T__'8715''8902'__14 → AgdaAny Source #
d_SRweak_310 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T_Kind_476 → T_Kind_476 → T__'8715''8902'__14 → AgdaAny Source #
du_SRweak_310 ∷ T_Ctx'8902'_2 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T_Kind_476 → T_Kind_476 → T__'8715''8902'__14 → AgdaAny Source #
d_SRApp_328 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → T__'8866''8902'__20 → T__'8846'__30 → AgdaAny → T__'8866''8902'__20 → AgdaAny → AgdaAny → AgdaAny Source #
du_SRApp_328 ∷ T_Ctx'8902'_2 → T_Kind_476 → T_Kind_476 → T__'8846'__30 → AgdaAny → T__'8866''8902'__20 → AgdaAny → AgdaAny → AgdaAny Source #
d_evalSR_358 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → T_Kind_476 → T__'8866''8902'__20 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → AgdaAny Source #
d_evalSR'45'List_370 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → [T__'8866''8902'__20] → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T__'91''8801''93'β__4 Source #
d_evalSR'45'VecList_384 ∷ T_Ctx'8902'_2 → T_Ctx'8902'_2 → Integer → T_Vec_24 → (T_Kind_476 → T__'8715''8902'__14 → T__'8866''8902'__20) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → (T_Kind_476 → T__'8715''8902'__14 → AgdaAny) → T__'10216''91''8801''93''10217'β__8 Source #