lean4-htt/src/library/tactic/simplifier
2016-07-09 10:11:12 -07:00
..
ceqv.cpp
ceqv.h
CMakeLists.txt feat(simplifier/simp_extensions): basic bookkeeping 2016-07-04 17:13:19 -07:00
init_module.cpp feat(simplifier/simp_extensions): basic bookkeeping 2016-07-04 17:13:19 -07:00
init_module.h
simp_extensions.cpp chore(simplifier/simp_extensions): remove commented block 2016-07-04 17:14:22 -07:00
simp_extensions.h feat(library/tactic/simplifier): basic simplifier extensions 2016-07-04 17:13:30 -07:00
simp_lemmas.cpp
simp_lemmas.h
simplifier.cpp fix(simplifier): need to instantiate mvars in results from simp extensions 2016-07-09 10:11:12 -07:00
simplifier.h feat(simplifier): take list of lemmas and tactic as args to simplify 2016-07-09 10:10:59 -07:00