lean4-htt/src/library/constructions
2018-09-03 17:41:19 -07:00
..
brec_on.cpp chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
brec_on.h refactor(library): definitional ==> constructions 2016-08-11 10:08:22 -07:00
cases_on.cpp chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
cases_on.h refactor(library): definitional ==> constructions 2016-08-11 10:08:22 -07:00
CMakeLists.txt chore(library/constructions): remove constructor (dead code) 2018-09-03 17:41:19 -07:00
init_module.cpp chore(library/constructions): remove injective 2018-09-03 17:38:13 -07:00
init_module.h refactor(library): definitional ==> constructions 2016-08-11 10:08:22 -07:00
no_confusion.cpp chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
no_confusion.h refactor(library): definitional ==> constructions 2016-08-11 10:08:22 -07:00
projection.cpp chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
projection.h feat(frontends/lean/structure_cmd): allow implicitness infer annotation and parameters in field declaration 2018-02-28 12:49:22 +01:00
rec_on.cpp chore(kernel): univ_param vs lparam, level_param_names ==> names, and other inconsistencies 2018-09-03 13:05:42 -07:00
rec_on.h refactor(library): definitional ==> constructions 2016-08-11 10:08:22 -07:00
util.cpp feat(util/name_generator): name generator prefix bookkeeping 2018-02-21 15:04:19 -08:00
util.h refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name 2018-02-21 15:04:19 -08:00