Documentation

d_Clauses_6 :: () #

d_Telescope_8 :: () #

d_getName_60 :: T_Term_154 -> Maybe AgdaAny #

d__'8943''10216''8759''10217'__70 :: Integer -> [T_Arg_88] -> [T_Arg_88] #

d__'8943''10181''8759''10182'__78 :: Integer -> [T_Arg_88] -> [T_Arg_88] #

d_stripPis_86 :: T_Term_154 -> T_Σ_14 #

d_prependLams_98 :: [T_Σ_14] -> T_Term_154 -> T_Term_154 #

d_prependHLams_112 :: [T_String_6] -> T_Term_154 -> T_Term_154 #

d_prependVLams_118 :: [T_String_6] -> T_Term_154 -> T_Term_154 #

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 #

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 #

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 #

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 #

du_clause'45'injective_178 :: T__'8801'__12 -> T_Σ_14 #

d_absurd'45'clause'45'injective'8321'_188 :: [T_Σ_14] -> [T_Σ_14] -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_absurd'45'clause'45'injective'8322'_198 :: [T_Σ_14] -> [T_Σ_14] -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_absurd'45'clause'45'injective_208 :: [T_Σ_14] -> [T_Σ_14] -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14 #

du_absurd'45'clause'45'injective_208 :: T__'8801'__12 -> T_Σ_14 #

d__'8799''45'AbsTerm__210 :: T_Abs_112 -> T_Abs_112 -> T_Dec_20 #

d__'8799''45'AbsType__212 :: T_Abs_112 -> T_Abs_112 -> T_Dec_20 #

d__'8799''45'ArgTerm__214 :: T_Arg_88 -> T_Arg_88 -> T_Dec_20 #

d__'8799''45'ArgType__216 :: T_Arg_88 -> T_Arg_88 -> T_Dec_20 #

d__'8799''45'Args__218 :: [T_Arg_88] -> [T_Arg_88] -> T_Dec_20 #

d__'8799''45'Clause__220 :: T_Clause_160 -> T_Clause_160 -> T_Dec_20 #

d__'8799''45'Clauses__222 :: [T_Clause_160] -> [T_Clause_160] -> T_Dec_20 #

d__'8799'__224 :: T_Term_154 -> T_Term_154 -> T_Dec_20 #

d__'8799''45'Sort__226 :: T_Sort_156 -> T_Sort_156 -> T_Dec_20 #

d__'8799''45'Patterns__228 :: [T_Arg_88] -> [T_Arg_88] -> T_Dec_20 #

d__'8799''45'Pattern__230 :: T_Pattern_158 -> T_Pattern_158 -> T_Dec_20 #

d__'8799''45'Telescope__280 :: [T_Σ_14] -> [T_Σ_14] -> T_Dec_20 #

d_var'45'injective'8321'_330 :: Integer -> Integer -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_var'45'injective'8322'_340 :: Integer -> Integer -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_var'45'injective_350 :: Integer -> Integer -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14 #

du_var'45'injective_350 :: T__'8801'__12 -> T_Σ_14 #

d_con'45'injective'8321'_360 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_con'45'injective'8322'_370 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_con'45'injective_380 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14 #

du_con'45'injective_380 :: T__'8801'__12 -> T_Σ_14 #

d_def'45'injective'8321'_390 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_def'45'injective'8322'_400 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_def'45'injective_410 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14 #

du_def'45'injective_410 :: T__'8801'__12 -> T_Σ_14 #

d_meta'45'injective'8321'_420 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_meta'45'injective'8322'_430 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_meta'45'injective_440 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14 #

du_meta'45'injective_440 :: T__'8801'__12 -> T_Σ_14 #

d_lam'45'injective'8321'_450 :: T_Visibility_48 -> T_Visibility_48 -> T_Abs_112 -> T_Abs_112 -> T__'8801'__12 -> T__'8801'__12 #

d_lam'45'injective'8322'_460 :: T_Visibility_48 -> T_Visibility_48 -> T_Abs_112 -> T_Abs_112 -> T__'8801'__12 -> T__'8801'__12 #

d_lam'45'injective_470 :: T_Visibility_48 -> T_Visibility_48 -> T_Abs_112 -> T_Abs_112 -> T__'8801'__12 -> T_Σ_14 #

du_lam'45'injective_470 :: T__'8801'__12 -> T_Σ_14 #

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 #

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 #

d_pat'45'lam'45'injective_500 :: [T_Clause_160] -> [T_Clause_160] -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14 #

du_pat'45'lam'45'injective_500 :: T__'8801'__12 -> T_Σ_14 #

d_pi'45'injective'8321'_510 :: T_Arg_88 -> T_Arg_88 -> T_Abs_112 -> T_Abs_112 -> T__'8801'__12 -> T__'8801'__12 #

d_pi'45'injective'8322'_520 :: T_Arg_88 -> T_Arg_88 -> T_Abs_112 -> T_Abs_112 -> T__'8801'__12 -> T__'8801'__12 #

d_pi'45'injective_530 :: T_Arg_88 -> T_Arg_88 -> T_Abs_112 -> T_Abs_112 -> T__'8801'__12 -> T_Σ_14 #

du_pi'45'injective_530 :: T__'8801'__12 -> T_Σ_14 #

d_sort'45'injective_536 :: T_Sort_156 -> T_Sort_156 -> T__'8801'__12 -> T__'8801'__12 #

d_lit'45'injective_542 :: T_Literal_124 -> T_Literal_124 -> T__'8801'__12 -> T__'8801'__12 #

d_set'45'injective_548 :: T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12 #

d_slit'45'injective_554 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_prop'45'injective_560 :: T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12 #

d_propLit'45'injective_566 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_inf'45'injective_572 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_pat'45'con'45'injective'8321'_1026 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_pat'45'con'45'injective'8322'_1036 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T__'8801'__12 #

d_pat'45'con'45'injective_1046 :: AgdaAny -> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14 #

du_pat'45'con'45'injective_1046 :: T__'8801'__12 -> T_Σ_14 #

d_pat'45'var'45'injective_1052 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #

d_pat'45'lit'45'injective_1058 :: T_Literal_124 -> T_Literal_124 -> T__'8801'__12 -> T__'8801'__12 #

d_proj'45'injective_1064 :: AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #

d_dot'45'injective_1070 :: T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12 #

d_absurd'45'injective_1076 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12 #