Documentation

d_ScopedTy_14 ∷ p → () Source #

data T_ScopedTy_14 Source #

d_Tel'8902'_36 ∷ Integer → Integer → () Source #

d_Weirdℕ_42 ∷ p → () Source #

data T_Weirdℕ_42 Source #

d_WeirdFin_56 ∷ p → p → () Source #

data T_WeirdFin_56 Source #

d_wtoℕ_78 ∷ Integer → T_Weirdℕ_42 → Integer Source #

du_wtoℕ_78 ∷ T_Weirdℕ_42 → Integer Source #

d_WeirdFintoℕ_88 ∷ Integer → T_Weirdℕ_42 → T_WeirdFin_56 → Integer Source #

du_WeirdFintoℕ_88 ∷ T_Weirdℕ_42 → T_WeirdFin_56 → Integer Source #

d_wtoℕTm_96 ∷ Integer → T_Weirdℕ_42 → Integer Source #

du_wtoℕTm_96 ∷ T_Weirdℕ_42 → Integer Source #

d_wtoℕTy_104 ∷ Integer → T_Weirdℕ_42 → Integer Source #

du_wtoℕTy_104 ∷ T_Weirdℕ_42 → Integer Source #

d_lookupWTm_116 ∷ Integer → Integer → T_Weirdℕ_42 → Maybe Integer Source #

du_lookupWTm_116 ∷ Integer → T_Weirdℕ_42 → Maybe Integer Source #

d_lookupWTy_138 ∷ Integer → Integer → T_Weirdℕ_42 → Maybe Integer Source #

du_lookupWTy_138 ∷ Integer → T_Weirdℕ_42 → Maybe Integer Source #

d_lookupWTm''_158 ∷ Integer → Integer → T_Weirdℕ_42 → Integer Source #

du_lookupWTm''_158 ∷ Integer → T_Weirdℕ_42 → Integer Source #

d_lookupWTy''_176 ∷ Integer → Integer → T_Weirdℕ_42 → Integer Source #

du_lookupWTy''_176 ∷ Integer → T_Weirdℕ_42 → Integer Source #

d_shifterTy_194 ∷ Integer → T_Weirdℕ_42 → T_RawTy_2 → T_RawTy_2 Source #

d_shifterTyList_200 ∷ Integer → T_Weirdℕ_42 → T_List_382 T_RawTy_2 → T_List_382 T_RawTy_2 Source #

d_shifterTyListList_206 ∷ Integer → T_Weirdℕ_42 → T_List_382 (T_List_382 T_RawTy_2) → T_List_382 (T_List_382 T_RawTy_2) Source #

d_shifter_272 ∷ Integer → T_Weirdℕ_42 → T_RawTm_30 → T_RawTm_30 Source #

d_shifterList_278 ∷ Integer → T_Weirdℕ_42 → T_List_382 T_RawTm_30 → T_List_382 T_RawTm_30 Source #

d_unshifterTy_360 ∷ Integer → T_Weirdℕ_42 → T_RawTy_2 → T_RawTy_2 Source #

d_unshifterTyList_366 ∷ Integer → T_Weirdℕ_42 → T_List_382 T_RawTy_2 → T_List_382 T_RawTy_2 Source #

d_unshifterTyListList_372 ∷ Integer → T_Weirdℕ_42 → T_List_382 (T_List_382 T_RawTy_2) → T_List_382 (T_List_382 T_RawTy_2) Source #

d_unshifter_434 ∷ Integer → T_Weirdℕ_42 → T_RawTm_30 → T_RawTm_30 Source #

d_unshifterList_440 ∷ Integer → T_Weirdℕ_42 → T_List_382 T_RawTm_30 → T_List_382 T_RawTm_30 Source #

d_ScopedTm_522 ∷ p → p → () Source #

data T_ScopedTm_522 Source #

d_Tel_568 ∷ Integer → T_Weirdℕ_42 → Integer → () Source #

type T_FreeVariableError_574 = FreeVariableError Source #

d_FreeVariableError_574 ∷ a Source #

d_ScopeError_576 ∷ () Source #

type T_ScopeError_576 = ScopeError Source #

pattern C_deBError_578 ∷ ScopeError Source #

pattern C_freeVariableError_580 ∷ FreeVariableError → ScopeError Source #

check_deBError_578 ∷ T_ScopeError_576 Source #

check_freeVariableError_580 ∷ T_FreeVariableError_574 → T_ScopeError_576 Source #

cover_ScopeError_576 ∷ ScopeError → () Source #

d_ℕtoFin_584 ∷ Integer → Integer → T_Either_6 T_ScopeError_576 T_Fin_10 Source #

d_ℕtoWeirdFin_596 ∷ Integer → T_Weirdℕ_42 → Integer → T_Either_6 T_ScopeError_576 T_WeirdFin_56 Source #

du_ℕtoWeirdFin_596 ∷ T_Weirdℕ_42 → Integer → T_Either_6 T_ScopeError_576 T_WeirdFin_56 Source #

d_scopeCheckTy_616 ∷ Integer → T_RawTy_2 → T_Either_6 T_ScopeError_576 T_ScopedTy_14 Source #

d_scopeCheckTyList_620 ∷ Integer → T_List_382 T_RawTy_2 → T_Either_6 T_ScopeError_576 (T_List_382 T_ScopedTy_14) Source #

d_scopeCheckTyListList_624 ∷ Integer → T_List_382 (T_List_382 T_RawTy_2) → T_Either_6 T_ScopeError_576 (T_List_382 (T_List_382 T_ScopedTy_14)) Source #

d_scopeCheckTm_686 ∷ Integer → T_Weirdℕ_42 → T_RawTm_30 → T_Either_6 T_ScopeError_576 T_ScopedTm_522 Source #

d_scopeCheckTmList_692 ∷ Integer → T_Weirdℕ_42 → T_List_382 T_RawTm_30 → T_Either_6 T_ScopeError_576 (T_List_382 T_ScopedTm_522) Source #

d_extricateScopeTy_780 ∷ Integer → T_ScopedTy_14 → T_RawTy_2 Source #

d_extricateScopeTyList_784 ∷ Integer → T_List_382 T_ScopedTy_14 → T_List_382 T_RawTy_2 Source #

d_extricateScopeTyListList_788 ∷ Integer → T_List_382 (T_List_382 T_ScopedTy_14) → T_List_382 (T_List_382 T_RawTy_2) Source #

d_extricateScope_828 ∷ Integer → T_Weirdℕ_42 → T_ScopedTm_522 → T_RawTm_30 Source #

d_extricateScopeList_834 ∷ Integer → T_Weirdℕ_42 → T_List_382 T_ScopedTm_522 → T_List_382 T_RawTm_30 Source #

d_uglyWeirdFin_888 ∷ Integer → T_Weirdℕ_42 → T_WeirdFin_56 → T_String_6 Source #

du_uglyWeirdFin_888 ∷ T_Weirdℕ_42 → T_WeirdFin_56 → T_String_6 Source #

d_uglyTmCon_894 ∷ T_TmCon_198 → T_String_6 Source #

d_showNat_902 ∷ Integer → T_String_6 Source #

d_uglyBuiltin_904 ∷ T_Builtin_2 → T_String_6 Source #

d_ugly_910 ∷ Integer → T_Weirdℕ_42 → T_ScopedTm_522 → T_String_6 Source #

du_ugly_910 ∷ T_Weirdℕ_42 → T_ScopedTm_522 → T_String_6 Source #