Leonardo de Moura b6051a6a03 feat(library/init/meta/congruence_tactics): add cc_dbg that display equivalence classes at failure		2016-12-25 10:46:15 -08:00
..
ac_tactics.lean
attribute.lean
backward.lean
comp_value_tactics.lean	feat(library): add mk_int_val_ne_proof	2016-12-24 15:22:31 -08:00
congr_lemma.lean
congruence_tactics.lean	feat(library/init/meta/congruence_tactics): add cc_dbg that display equivalence classes at failure	2016-12-25 10:46:15 -08:00
constructor_tactic.lean
contradiction_tactic.lean
converter.lean
decl_cmds.lean
declaration.lean
default.lean	feat(library/init/meta,library/tactic/congruence): add congruence closure lean API	2016-12-22 16:26:17 -08:00
environment.lean
exceptional.lean
expr.lean
format.lean
fun_info.lean
injection_tactic.lean
interactive.lean
level.lean
match_tactic.lean
mk_dec_eq_instance.lean
mk_has_sizeof_instance.lean
mk_inhabited_instance.lean
name.lean
occurrences.lean
options.lean
pexpr.lean
rb_map.lean
rec_util.lean
relation_tactics.lean
rewrite_tactic.lean
set_get_option_tactics.lean
simp_tactic.lean
tactic.lean
task.lean
vm.lean