Mario Carneiro 6e88119f55 feat(init/meta/injection_tactic): better injection tactic ... (1) The lhs and rhs will be reduced to whnf before getting the constructor apps (2) If the lhs and rhs are distinct constructors, it discharges the goal by contradiction (3) The interactive injection tactic will try to close the goal by assumption if successful		2017-05-27 04:59:40 -04:00
..
basic.lean	chore(*): remove pos_num and num from stdlib	2017-05-25 18:24:16 -07:00
default.lean	feat(lib/init/data/nat): add function pow and a Galois connection between div and mul	2017-03-12 09:38:19 -07:00
div.lean	refactor(library): avoid auxiliary definitions such as add/mul/le/etc	2017-05-01 08:52:19 -07:00
lemmas.lean	feat(init/meta/injection_tactic): better injection tactic	2017-05-27 04:59:40 -04:00
pow.lean	feat(library/data/list, library/data/array): theorems needed for new hash_map	2017-05-16 14:38:43 -07:00