lean2

Author	SHA1	Message	Date
Leonardo de Moura	49323ab598	feat(library/util): add mk_symm	2015-02-04 13:44:55 -08:00
Leonardo de Moura	4c7a17cc4a	refactor(library/tactic/class_instance_synth): move has_expr_metavar_relaxed to util	2015-02-01 10:59:27 -08:00
Leonardo de Moura	27f6bfd3f0	refactor(*): add file constants.txt with all constants used by the Lean binary	2015-01-23 16:50:32 -08:00
Leonardo de Moura	a53098385c	refactor(frontends/lean/type_util): move infer_implicit_params to library	2015-01-21 17:22:41 -08:00
Leonardo de Moura	b6750e9d29	feat(library/util): add auxiliary functions	2015-01-20 15:44:58 -08:00
Leonardo de Moura	98a856373d	feat(library/util): add dec_level auxiliary procedure	2015-01-04 13:25:58 -08:00
Leonardo de Moura	7f7d318b22	feat(library/definitional/equations): add dependent pattern matching compilation	2015-01-02 22:06:40 -08:00
Leonardo de Moura	1d79cb9c07	fix(library/tactic/inversion_tactic): fix bug in 'cases' tactic for HoTT library	2014-12-22 09:40:15 -08:00
Leonardo de Moura	2070ac849c	feat(library/util): add get_intro_rule_names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-12-20 11:31:48 -08:00
Leonardo de Moura	8c63045492	feat(library/util): add more auxiliary procedures	2014-12-19 22:00:25 -08:00
Leonardo de Moura	9bd74689be	feat(library/util): add mk_refl	2014-12-19 13:54:12 -08:00
Leonardo de Moura	a97bef7df2	feat(library/util): add mk_heq	2014-12-19 13:54:12 -08:00
Leonardo de Moura	1ca8723c54	refactor(library/util): allow mk_telescopic_eq to be used with (terms, locals)	2014-12-19 13:54:12 -08:00
Leonardo de Moura	8939351903	refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception	2014-12-15 19:22:17 -08:00
Leonardo de Moura	e897bbdeb9	feat(library/util): add auxiliary functions for creating tuples (using sigma types)	2014-12-11 17:31:47 -08:00
Leonardo de Moura	d98aabe9ab	refactor(library): move library/definitional/util module to library	2014-12-10 11:23:23 -08:00

16 commits