Leonardo de Moura 7f43d01703 fix: assertion violation		2020-07-24 14:54:20 -07:00
..
brec_on.cpp	feat: export "constructions"	2020-07-15 16:32:23 -07:00
brec_on.h	feat(library/constructions/brec_on): add brec_on and binduction_on for new inductive datatype module	2018-09-05 14:46:03 -07:00
cases_on.cpp	feat: export "constructions"	2020-07-15 16:32:23 -07:00
cases_on.h	feat(*): use new inductive datatype module	2018-09-06 18:09: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
no_confusion.cpp	feat: export "constructions"	2020-07-15 16:32:23 -07:00
no_confusion.h	feat(*): use new inductive datatype module	2018-09-06 18:09:22 -07:00
projection.cpp	fix: assertion violation	2020-07-24 14:54:20 -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	feat: export "constructions"	2020-07-15 16:32:23 -07:00
rec_on.h	feat(*): use new inductive datatype module	2018-09-06 18:09:22 -07:00
util.cpp	feat: use kernel projections in constructions	2019-11-04 03:38:57 -08:00
util.h	chore(kernel): move abstract_type_context to library	2018-09-08 08:29:51 -07:00