Documentation

d_Clauses_6 ∷ () Source #

d_Telescope_8 ∷ () Source #

d_getName_60 ∷ T_Term_154 → Maybe AgdaAny Source #

d__'8943''10216''8759''10217'__70 ∷ Integer → [T_Arg_88] → [T_Arg_88] Source #

d__'8943''10181''8759''10182'__78 ∷ Integer → [T_Arg_88] → [T_Arg_88] Source #

d_stripPis_86 ∷ T_Term_154 → T_Σ_14 Source #

d_prependLams_98 ∷ [T_Σ_14] → T_Term_154 → T_Term_154 Source #

d_prependHLams_112 ∷ [T_String_6] → T_Term_154 → T_Term_154 Source #

d_prependVLams_118 ∷ [T_String_6] → T_Term_154 → T_Term_154 Source #

d_clause'45'injective'8321'_136 ∷ [T_Σ_14] → [T_Σ_14] → [T_Arg_88] → [T_Arg_88] → T_Term_154 → T_Term_154 → T__'8801'__12 → T__'8801'__12 Source #

d_clause'45'injective'8322'_150 ∷ [T_Σ_14] → [T_Σ_14] → [T_Arg_88] → [T_Arg_88] → T_Term_154 → T_Term_154 → T__'8801'__12 → T__'8801'__12 Source #

d_clause'45'injective'8323'_164 ∷ [T_Σ_14] → [T_Σ_14] → [T_Arg_88] → [T_Arg_88] → T_Term_154 → T_Term_154 → T__'8801'__12 → T__'8801'__12 Source #

d_clause'45'injective_178 ∷ [T_Σ_14] → [T_Σ_14] → [T_Arg_88] → [T_Arg_88] → T_Term_154 → T_Term_154 → T__'8801'__12 → T_Σ_14 Source #

du_clause'45'injective_178 ∷ T__'8801'__12 → T_Σ_14 Source #

d_absurd'45'clause'45'injective'8321'_188 ∷ [T_Σ_14] → [T_Σ_14] → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_absurd'45'clause'45'injective'8322'_198 ∷ [T_Σ_14] → [T_Σ_14] → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_absurd'45'clause'45'injective_208 ∷ [T_Σ_14] → [T_Σ_14] → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T_Σ_14 Source #

du_absurd'45'clause'45'injective_208 ∷ T__'8801'__12 → T_Σ_14 Source #

d__'8799''45'AbsTerm__210 ∷ T_Abs_112 → T_Abs_112 → T_Dec_20 Source #

d__'8799''45'AbsType__212 ∷ T_Abs_112 → T_Abs_112 → T_Dec_20 Source #

d__'8799''45'ArgTerm__214 ∷ T_Arg_88 → T_Arg_88 → T_Dec_20 Source #

d__'8799''45'ArgType__216 ∷ T_Arg_88 → T_Arg_88 → T_Dec_20 Source #

d__'8799''45'Args__218 ∷ [T_Arg_88] → [T_Arg_88] → T_Dec_20 Source #

d__'8799''45'Clause__220 ∷ T_Clause_160 → T_Clause_160 → T_Dec_20 Source #

d__'8799''45'Clauses__222 ∷ [T_Clause_160] → [T_Clause_160] → T_Dec_20 Source #

d__'8799'__224 ∷ T_Term_154 → T_Term_154 → T_Dec_20 Source #

d__'8799''45'Sort__226 ∷ T_Sort_156 → T_Sort_156 → T_Dec_20 Source #

d__'8799''45'Patterns__228 ∷ [T_Arg_88] → [T_Arg_88] → T_Dec_20 Source #

d__'8799''45'Pattern__230 ∷ T_Pattern_158 → T_Pattern_158 → T_Dec_20 Source #

d__'8799''45'Telescope__280 ∷ [T_Σ_14] → [T_Σ_14] → T_Dec_20 Source #

d_var'45'injective'8321'_330 ∷ Integer → Integer → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_var'45'injective'8322'_340 ∷ Integer → Integer → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_var'45'injective_350 ∷ Integer → Integer → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T_Σ_14 Source #

du_var'45'injective_350 ∷ T__'8801'__12 → T_Σ_14 Source #

d_con'45'injective'8321'_360 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_con'45'injective'8322'_370 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_con'45'injective_380 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T_Σ_14 Source #

du_con'45'injective_380 ∷ T__'8801'__12 → T_Σ_14 Source #

d_def'45'injective'8321'_390 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_def'45'injective'8322'_400 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_def'45'injective_410 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T_Σ_14 Source #

du_def'45'injective_410 ∷ T__'8801'__12 → T_Σ_14 Source #

d_meta'45'injective'8321'_420 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_meta'45'injective'8322'_430 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_meta'45'injective_440 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T_Σ_14 Source #

du_meta'45'injective_440 ∷ T__'8801'__12 → T_Σ_14 Source #

d_lam'45'injective'8321'_450 ∷ T_Visibility_48 → T_Visibility_48 → T_Abs_112 → T_Abs_112 → T__'8801'__12 → T__'8801'__12 Source #

d_lam'45'injective'8322'_460 ∷ T_Visibility_48 → T_Visibility_48 → T_Abs_112 → T_Abs_112 → T__'8801'__12 → T__'8801'__12 Source #

d_lam'45'injective_470 ∷ T_Visibility_48 → T_Visibility_48 → T_Abs_112 → T_Abs_112 → T__'8801'__12 → T_Σ_14 Source #

du_lam'45'injective_470 ∷ T__'8801'__12 → T_Σ_14 Source #

d_pat'45'lam'45'injective'8321'_480 ∷ [T_Clause_160] → [T_Clause_160] → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_pat'45'lam'45'injective'8322'_490 ∷ [T_Clause_160] → [T_Clause_160] → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_pat'45'lam'45'injective_500 ∷ [T_Clause_160] → [T_Clause_160] → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T_Σ_14 Source #

du_pat'45'lam'45'injective_500 ∷ T__'8801'__12 → T_Σ_14 Source #

d_pi'45'injective'8321'_510 ∷ T_Arg_88 → T_Arg_88 → T_Abs_112 → T_Abs_112 → T__'8801'__12 → T__'8801'__12 Source #

d_pi'45'injective'8322'_520 ∷ T_Arg_88 → T_Arg_88 → T_Abs_112 → T_Abs_112 → T__'8801'__12 → T__'8801'__12 Source #

d_pi'45'injective_530 ∷ T_Arg_88 → T_Arg_88 → T_Abs_112 → T_Abs_112 → T__'8801'__12 → T_Σ_14 Source #

du_pi'45'injective_530 ∷ T__'8801'__12 → T_Σ_14 Source #

d_sort'45'injective_536 ∷ T_Sort_156 → T_Sort_156 → T__'8801'__12 → T__'8801'__12 Source #

d_lit'45'injective_542 ∷ T_Literal_124 → T_Literal_124 → T__'8801'__12 → T__'8801'__12 Source #

d_set'45'injective_548 ∷ T_Term_154 → T_Term_154 → T__'8801'__12 → T__'8801'__12 Source #

d_slit'45'injective_554 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_prop'45'injective_560 ∷ T_Term_154 → T_Term_154 → T__'8801'__12 → T__'8801'__12 Source #

d_propLit'45'injective_566 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_inf'45'injective_572 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_pat'45'con'45'injective'8321'_1026 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_pat'45'con'45'injective'8322'_1036 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T__'8801'__12 Source #

d_pat'45'con'45'injective_1046 ∷ AgdaAny → AgdaAny → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T_Σ_14 Source #

du_pat'45'con'45'injective_1046 ∷ T__'8801'__12 → T_Σ_14 Source #

d_pat'45'var'45'injective_1052 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_pat'45'lit'45'injective_1058 ∷ T_Literal_124 → T_Literal_124 → T__'8801'__12 → T__'8801'__12 Source #

d_proj'45'injective_1064 ∷ AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_dot'45'injective_1070 ∷ T_Term_154 → T_Term_154 → T__'8801'__12 → T__'8801'__12 Source #

d_absurd'45'injective_1076 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #