| .. |
|
brec_on.cpp
|
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
|
2018-02-21 15:04:19 -08:00 |
|
brec_on.h
|
refactor(library): definitional ==> constructions
|
2016-08-11 10:08:22 -07:00 |
|
cases_on.cpp
|
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
|
2018-02-21 15:04:19 -08:00 |
|
cases_on.h
|
refactor(library): definitional ==> constructions
|
2016-08-11 10:08:22 -07:00 |
|
CMakeLists.txt
|
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
|
2018-02-21 15:04:19 -08:00 |
|
constructor.cpp
|
feat(library/tactic/simplify): add support for generalized inductive datatypes
|
2018-01-12 11:51:49 -08:00 |
|
constructor.h
|
feat(library/tactic/smt/congruence_closure): propagate disequalities
|
2017-01-03 14:53:27 -08:00 |
|
drec.cpp
|
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
|
2018-02-21 15:04:19 -08:00 |
|
drec.h
|
feat(library/constructions,library/inductive_compiler): automatically generate dependent eliminator for inductive predicates
|
2017-02-28 20:58:04 -08:00 |
|
has_sizeof.cpp
|
fix(library/type_context): remove unsafe type_context::operator=(type_context &&)
|
2018-02-26 12:28:22 -08:00 |
|
has_sizeof.h
|
refactor(library/tactic/simp_lemmas): simp set generation should not be affected by transparency setting
|
2017-07-01 12:54:37 -07:00 |
|
init_module.cpp
|
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
|
2018-02-21 15:04:19 -08:00 |
|
init_module.h
|
refactor(library): definitional ==> constructions
|
2016-08-11 10:08:22 -07:00 |
|
injective.cpp
|
feat(library/constructions/injective): automatically generate auxiliary lemma *.inj_eq for constructors
|
2018-01-12 16:41:12 -08:00 |
|
injective.h
|
feat(library/constructions/injective): automatically generate auxiliary lemma *.inj_eq for constructors
|
2018-01-12 16:41:12 -08:00 |
|
no_confusion.cpp
|
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
|
2018-02-21 15:04:19 -08:00 |
|
no_confusion.h
|
refactor(library): definitional ==> constructions
|
2016-08-11 10:08:22 -07:00 |
|
projection.cpp
|
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
|
2018-02-21 15:04:19 -08:00 |
|
projection.h
|
refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields
|
2017-04-24 19:35:15 +02:00 |
|
rec_on.cpp
|
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
|
2018-02-21 15:04:19 -08: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 |
e53ef3c335