Documentation

d_Clauses_4 ∷ () Source #

d_Telescope_6 ∷ () Source #

d_getName_58 ∷ T_Term_154 → Maybe AgdaAny Source #

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

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

d_clause'45'injective'8321'_96 ∷ [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'_110 ∷ [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'_124 ∷ [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_138 ∷ [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_138 ∷ T__'8801'__12 → T_Σ_14 Source #

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

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

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

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

d__'8799''45'AbsTerm__170 ∷ T_Abs_112 → T_Abs_112 → T_Dec_32 Source #

d__'8799''45'AbsType__172 ∷ T_Abs_112 → T_Abs_112 → T_Dec_32 Source #

d__'8799''45'ArgTerm__174 ∷ T_Arg_88 → T_Arg_88 → T_Dec_32 Source #

d__'8799''45'ArgType__176 ∷ T_Arg_88 → T_Arg_88 → T_Dec_32 Source #

d__'8799''45'Args__178 ∷ [T_Arg_88] → [T_Arg_88] → T_Dec_32 Source #

d__'8799''45'Clause__180 ∷ T_Clause_160 → T_Clause_160 → T_Dec_32 Source #

d__'8799''45'Clauses__182 ∷ [T_Clause_160] → [T_Clause_160] → T_Dec_32 Source #

d__'8799'__184 ∷ T_Term_154 → T_Term_154 → T_Dec_32 Source #

d__'8799''45'Sort__186 ∷ T_Sort_156 → T_Sort_156 → T_Dec_32 Source #

d__'8799''45'Patterns__188 ∷ [T_Arg_88] → [T_Arg_88] → T_Dec_32 Source #

d__'8799''45'Pattern__190 ∷ T_Pattern_158 → T_Pattern_158 → T_Dec_32 Source #

d__'8799''45'Telescope__240 ∷ [T_Σ_14] → [T_Σ_14] → T_Dec_32 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_pat'45'lam'45'injective'8321'_440 ∷ [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'_450 ∷ [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_460 ∷ [T_Clause_160] → [T_Clause_160] → [T_Arg_88] → [T_Arg_88] → T__'8801'__12 → T_Σ_14 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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