Leonardo de Moura 02fb2c9c8a feat(library/init): add 'guard' and helper typeclasses		2016-07-07 00:52:52 -07:00
..
expensive
extra	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
hott	refactor(frontends/lean): remove 'by+' and 'begin+' tokens	2016-02-29 13:45:43 -08:00
interactive	chore(tests/lean/interactive/alias): fix test expected output	2016-06-27 14:37:18 +01:00
perf	test(tests/lean/run): add three perf tests	2016-07-05 19:48:20 -07:00
run	feat(frontends/lean): add parent classes to local context in struct definitions	2016-07-05 19:22:08 -07:00
slow	chore(tests/lean): disable tests	2016-06-10 18:29:41 -07:00
trust0	fix(test*.sh): allow spaces in filename	2015-03-28 23:29:52 -04:00
438.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
438.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
480.hlean	fix(frontends/lean/pp): abbreviations with too much arguments	2015-03-23 12:16:25 -07:00
480.hlean.expected.out	fix(frontends/lean/pp): abbreviations with too much arguments	2015-03-23 12:16:25 -07:00
487.hlean	feat(frontends/lean): uniform notation for lists in tactics	2015-03-27 17:54:48 -07:00
487.hlean.expected.out	fix(tests): update tests because [unfold-c] attribute has been added to some definitions	2015-05-18 15:59:55 -07:00
531.hlean	fix(tests/lean): adjust tests to reflect changes in the elaboration process	2015-06-26 17:18:30 -07:00
531.hlean.expected.out	fix(tests/lean): adjust tests to reflect changes in the elaboration process	2015-06-26 17:18:30 -07:00
550.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
550.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
559.lean	refactor(frontends/lean): disable '!' operator, and adjust standard library	2016-07-02 01:41:46 +01:00
559.lean.expected.out	fix(frontends/lean/util): assertion violation	2015-04-24 15:09:23 -07:00
571.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
571.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
582.hlean	fix(frontends/lean/structure_cmd): 'structure' command must set unfold-c attribute for auxiliary recursors	2015-05-07 09:09:07 -07:00
582.hlean.expected.out	fix(frontends/lean/structure_cmd): 'structure' command must set unfold-c attribute for auxiliary recursors	2015-05-07 09:09:07 -07:00
584a.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
584a.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
584b.lean	fix(frontends/lean/parser): fixes #584	2015-05-07 14:24:30 -07:00
584b.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
584c.lean	fix(frontends/lean/parser): fixes #584	2015-05-07 14:24:30 -07:00
584c.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
587.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
587.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
604.lean	fix(frontends/lean/pp): print notation produces incorrect output	2015-05-19 09:57:13 -07:00
604.lean.expected.out	fix(frontends/lean/pp): print notation produces incorrect output	2015-05-19 09:57:13 -07:00
608.hlean	feat(frontends/lean): print all options for overloaded identifier	2015-05-18 17:14:17 -07:00
608.hlean.expected.out	feat(library/attribute_manager, frontends/lean/builtin_cmds): use attribute manager information when pretty print definitions	2015-12-17 21:16:31 -08:00
626a.lean	feat(frontends/lean/scanner): disallow superscripts in identifiers	2016-01-26 18:46:40 -08:00
626a.lean.expected.out	fix(frontends/lean/elaborator): closes #771	2015-08-07 13:29:22 -07:00
626b.hlean	fix(tests/lean): adjust tests to reflect changes in the HoTT library	2015-09-25 09:46:51 -07:00
626b.hlean.expected.out	fix(tests): fix tests to reflect changes	2015-05-26 21:37:02 -07:00
626c.lean	fix(frontends/lean/scanner): another bug related to issue #626	2015-05-26 13:39:42 -07:00
626c.lean.expected.out	fix(frontends/lean/elaborator): closes #771	2015-08-07 13:29:22 -07:00
634.lean	fix(frontends/lean/pp): fixes #634	2015-05-28 19:43:49 -07:00
634.lean.expected.out	fix(frontends/lean/pp): fixes #634	2015-05-29 14:07:38 -07:00
634b.lean	fix(frontends/lean/pp): fixes #634	2015-05-29 14:07:38 -07:00
634b.lean.expected.out	fix(frontends/lean/pp): fixes #634	2015-05-29 14:07:38 -07:00
634c.lean	fix(frontends/lean/pp): fixes #634	2015-05-29 14:07:38 -07:00
634c.lean.expected.out	fix(frontends/lean/pp): fixes #634	2015-05-29 14:07:38 -07:00
634d.lean	test(tests/lean): add missing test for issue #634	2015-05-29 15:13:43 -07:00
634d.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
640.hlean	feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'	2015-07-07 16:37:06 -07:00
640.hlean.expected.out	renaming(hit): rename type_quotient to quotient, and quotient to set_quotient	2015-06-04 20:14:13 -04:00
640a.hlean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
640a.hlean.expected.out	fix(frontends/lean/pp): abbreviation with parameters	2015-05-29 15:13:31 -07:00
640b.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
640b.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
644.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
644.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
652.lean	fix(frontends/lean): fixes #652	2015-06-03 21:53:51 -07:00
652.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
669.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
669.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
671.lean	fix(frontends/lean/builtin_cmds): fixes #671	2015-06-13 11:35:03 -07:00
671.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
689.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
689.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
690.hlean	fix(library/tactic/induction_tactic.cpp): condition for checking whether 'induction' tatic is applicable or not	2015-06-28 13:07:02 -07:00
690.hlean.expected.out	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
691.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
691.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
693.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
693.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
704.lean	feat(library/simplifier/simp_rule_set): add priorities for simp and congr rules	2015-11-16 22:34:06 -08:00
704.lean.expected.out	fix(library/logic/axioms/prop_decidable): fixes #704	2015-06-26 19:14:36 -07:00
712.lean	feat(frontends/lean/notation_cmd): allow local notation to override reserved notation	2015-07-07 17:30:46 -07:00
712.lean.expected.out	chore(tests/lean): fix tests	2016-06-16 18:47:23 -07:00
770.hlean	fix(tests): fix tests after port	2015-12-09 12:36:11 -08:00
770.hlean.expected.out	fix(tests): fix tests after port	2015-12-09 12:36:11 -08:00
771.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
771.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
775.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
775.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
778.hlean	feat(library/tactic/tactic): apply substitution in 'then' combinator	2015-08-08 03:42:21 -07:00
778.hlean.expected.out	feat(library/tactic/tactic): apply substitution in 'then' combinator	2015-08-08 03:42:21 -07:00
779.hlean	fix(library/tactic/exact_tactic): fixes #779	2015-08-07 13:29:22 -07:00
779.hlean.expected.out	fix(library/tactic/exact_tactic): fixes #779	2015-08-07 13:29:22 -07:00
852.hlean	fix(library/tc_multigraph): avoid name collisions	2016-02-04 13:15:42 -08:00
852.hlean.expected.out	fix(library/tc_multigraph): avoid name collisions	2016-02-04 13:15:42 -08:00
858.lean	fix(frontends/lean/parser): fixes #858	2015-12-10 10:31:14 -08:00
858.lean.expected.out	fix(frontends/lean/parser): fixes #858	2015-12-10 10:31:14 -08:00
893.hlean	fix(library/tactic/induction_tactic): fixes #893	2015-12-10 10:11:55 -08:00
893.hlean.expected.out	fix(library/tactic/induction_tactic): fixes #893	2015-12-10 10:11:55 -08:00
955.lean	chore(library/pp_options): reduce pp default limits	2016-02-04 14:55:21 -08:00
955.lean.expected.out	chore(library/pp_options): reduce pp default limits	2016-02-04 14:55:21 -08:00
abbrev1.lean	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
abbrev1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
abbrev2.lean	fix(frontends/lean/pp): bugs when pretty printing abbreviations	2015-02-10 19:06:09 -08:00
abbrev2.lean.expected.out	feat(frontends/lean): print all options for overloaded identifier	2015-05-18 17:14:17 -07:00
abbrev_paren.hlean	fix(tests): adjust tests to reflect changes in the HoTT library	2015-04-29 10:15:13 -07:00
abbrev_paren.hlean.expected.out	feat(frontends/lean): apply eta-reduction in postprocessing step	2015-06-10 16:29:30 -07:00
acc.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
acc.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
acc_rec_bug.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
acc_rec_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
alias.lean
alias.lean.expected.out
alias2.lean
alias2.lean.expected.out
apply_fail.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
apply_fail.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
assert_fail.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
assert_fail.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
assert_tac2.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
assert_tac2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
assert_tac3.lean	feat(tactic/init/meta/tactic): normalize assert, define tactic names	2016-06-21 17:50:30 -07:00
assert_tac3.lean.expected.out	fix(library/tactic/tactic_state): consume solved goals	2016-06-17 15:19:50 -07:00
attr_at1.lean	feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces	2015-12-05 11:15:02 -08:00
attr_at1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
attr_at2.lean	feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces	2015-12-05 11:15:02 -08:00
attr_at2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
attr_at3.lean	test(tests/lean/attr_at3): add test for 'attribute ... at ...'	2015-12-05 11:17:42 -08:00
attr_at3.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
auto_include.lean	feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included)	2015-12-13 13:20:54 -08:00
auto_include.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
backward_rule1.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
backward_rule1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
bad_class.lean	refactor(frontends/lean): disable '!' operator, and adjust standard library	2016-07-02 01:41:46 +01:00
bad_class.lean.expected.out	feat(library/class): allow any constant to be marked as a class	2015-06-17 16:26:45 -07:00
bad_end.lean
bad_end.lean.expected.out	feat(frontends/lean): remove 'context' command	2015-04-22 11:32:02 -07:00
bad_eqns.lean	feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed	2015-03-13 14:47:21 -07:00
bad_eqns.lean.expected.out	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-05-10 11:10:38 -07:00
bad_id.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
bad_id.lean.expected.out	feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1'	2014-11-09 12:55:13 -08:00
bad_notation.lean	test(tests/lean): remove data.nat dependency	2014-12-23 17:42:56 -08:00
bad_notation.lean.expected.out
bad_open.lean	refactor(*): normalize metaclass names	2015-12-28 10:39:15 -08:00
bad_open.lean.expected.out	refactor(*): normalize metaclass names	2015-12-28 10:39:15 -08:00
bad_pattern.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
bad_pattern.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
bad_pattern2.lean	feat(frontends/lean/decl_cmds): pattern variables must be atomic	2016-06-29 07:34:36 +01:00
bad_pattern2.lean.expected.out	feat(frontends/lean/decl_cmds): pattern variables must be atomic	2016-06-29 07:34:36 +01:00
bad_print.lean	test(tests/lean): add more tests for error messages	2015-02-01 20:04:22 -08:00
bad_print.lean.expected.out	test(tests/lean): add more tests for error messages	2015-02-01 20:04:22 -08:00
bad_quoted_symbol.lean	feat(frontends/lean/scanner): add more checks to read_quoted_symbol	2015-10-13 09:52:35 -07:00
bad_quoted_symbol.lean.expected.out	chore(tests/lean): fix tests	2016-06-16 18:47:23 -07:00
bad_set_option.lean	test(tests/lean/bad_set_option): add tests for bad 'set_option' command	2015-02-01 20:20:35 -08:00
bad_set_option.lean.expected.out	test(tests/lean/bad_set_option): add tests for bad 'set_option' command	2015-02-01 20:20:35 -08:00
bad_structures.lean	feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command	2016-02-22 16:09:44 -08:00
bad_structures.lean.expected.out	fix(src/frontends/lean/structure_cmd): fixes #1036	2016-06-14 17:52:31 -07:00
bad_structures2.lean	feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command	2016-02-22 16:09:44 -08:00
bad_structures2.lean.expected.out	feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command	2016-02-22 16:09:44 -08:00
beginend_bug.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
beginend_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
blast_back2.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
blast_back2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
blast_cc_not_provable.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
blast_cc_not_provable.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
bug1.lean	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
bug1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
calc1.lean	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
calc1.lean.expected.out	refactor(frontends/lean/calc): no overloading in calc steps	2016-03-03 15:00:51 -08:00
cases_failure.hlean	fix(library/tactic/inversion_tactic): type incorrect term being built by 'cases' tactic	2015-04-20 19:24:52 -07:00
cases_failure.hlean.expected.out	feat(frontends/lean): apply eta-reduction in postprocessing step	2015-06-10 16:29:30 -07:00
cases_tac.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
cases_tac.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
change1.lean	refactor(library/tactic/subst_tactic): subst take a local instead of a name	2016-06-22 15:13:49 -07:00
change1.lean.expected.out	feat(library/tactic): add 'change' tactic	2016-06-17 13:21:52 -07:00
change2.lean	refactor(library/tactic/subst_tactic): subst take a local instead of a name	2016-06-22 15:13:49 -07:00
change2.lean.expected.out	feat(library/tactic/defeq_simplifier): invoke defeq_canonize from defeq_simp	2016-06-24 14:46:43 -07:00
change_tac_fail.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
change_tac_fail.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
check.lean
check.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
check2.lean	fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming	2014-10-26 19:19:45 -07:00
check2.lean.expected.out	feat(frontends/lean): display metavariable application arguments in check command	2014-10-30 13:28:25 -07:00
check_expr.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
check_expr.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
choice_expl.lean	feat(frontends/lean/builtin_exprs): simplify '@' and '@@'	2016-07-02 11:08:18 +01:00
choice_expl.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
cls_err.lean	chore(tests): remove most occurrences of 'context' command from the test suite	2015-04-21 19:33:21 -07:00
cls_err.lean.expected.out	feat(library/tactic/goal): add option pp.compact_goals	2014-10-28 16:30:37 -07:00
coe.lean	fix(tests/lean): adjust some tests to changes in the standard library	2015-11-08 14:04:56 -08:00
coe.lean.expected.out
combinators1.lean	feat(library/init/meta/tactic): add 'focus', 'first', 'solve' and LCF-style AND_THEN tactical	2016-06-29 01:07:41 +01:00
combinators1.lean.expected.out	feat(library/init/meta/tactic): add 'focus', 'first', 'solve' and LCF-style AND_THEN tactical	2016-06-29 01:07:41 +01:00
config.hlean	fix(tests/lean): add missing file	2015-03-23 11:35:39 -07:00
config.hlean.expected.out	fix(tests/lean): add missing file	2015-03-23 11:35:39 -07:00
config.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
config.lean.expected.out
congr_error_msg.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
congr_error_msg.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
congr_print.lean	feat(frontends/lean): display '[congr]' attribute when printing theorems	2015-07-23 18:52:59 -07:00
congr_print.lean.expected.out	refactor(simplifier): port skeleton to new tactic framework	2016-06-24 15:20:40 -07:00
const.lean	feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables	2015-05-18 15:45:23 -07:00
const.lean.expected.out
constr_tac_errors.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
constr_tac_errors.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
crash.lean	chore(tests): remove most occurrences of 'context' command from the test suite	2015-04-21 19:33:21 -07:00
crash.lean.expected.out	feat(frontends/lean): apply eta-reduction in postprocessing step	2015-06-10 16:29:30 -07:00
ctx.lean	feat(library/tactic/goal): when listing context/goal variables, collect vars of same type in one line	2015-01-13 11:14:44 -08:00
ctx.lean.expected.out	fix(tests/lean): tests	2016-06-14 21:52:52 -07:00
ctxopt.lean	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
ctxopt.lean.expected.out	feat(frontends/lean/parser): restore config options in the end of sections/namespaces	2015-12-09 11:24:37 -08:00
defeq1.lean	refactor(library/init/meta/tactic): merge trace, trace_fmt and trace_expr	2016-06-23 09:29:42 -07:00
defeq1.lean.expected.out	feat(library/tactic): add tactic.defeq_simp	2016-06-17 11:20:15 -07:00
defeq_simp1.lean	feat(library/tactic/defeq_simplifier): invoke defeq_canonize from defeq_simp	2016-06-24 14:46:43 -07:00
defeq_simp1.lean.expected.out	feat(library/tactic/defeq_simplifier): invoke defeq_canonize from defeq_simp	2016-06-24 14:46:43 -07:00
defeq_simp2.lean	feat(library/tactic/defeq_simplifier): invoke defeq_canonize from defeq_simp	2016-06-24 14:46:43 -07:00
defeq_simp2.lean.expected.out	feat(library/tactic/defeq_simplifier): invoke defeq_canonize from defeq_simp	2016-06-24 14:46:43 -07:00
defeq_simp_lemmas1.lean	feat(library/blast/blast): use defeq_simplifier to normalize	2016-03-01 13:44:33 -08:00
defeq_simp_lemmas1.lean.expected.out	feat(library/blast/blast): use defeq_simplifier to normalize	2016-03-01 13:44:33 -08:00
defeq_simp_lemmas2.lean	feat(library/blast/blast): use defeq_simplifier to normalize	2016-03-01 13:44:33 -08:00
defeq_simp_lemmas2.lean.expected.out	feat(library/blast/blast): use defeq_simplifier to normalize	2016-03-01 13:44:33 -08:00
empty.lean	refactor(library/logic): move logic/choice.lean to init/classical.lean	2015-08-12 18:37:33 -07:00
empty.lean.expected.out	feat(library): add 'noncomputable' keyword for the standard library	2015-07-28 21:56:35 -07:00
empty_thm.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
empty_thm.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
eq_class_error.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
eq_class_error.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
error_full_names.lean	feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations	2015-02-25 17:00:10 -08:00
error_full_names.lean.expected.out	fix(tests/lean): adjust some tests to changes in the standard library	2015-11-08 14:04:56 -08:00
error_loc_bug.lean	refactor(frontends/lean): disable '!' operator, and adjust standard library	2016-07-02 01:41:46 +01:00
error_loc_bug.lean.expected.out	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-05-10 11:10:38 -07:00
error_pos_bug.lean
error_pos_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
error_pos_bug2.lean	refactor(library): remove unifier_plugin	2016-03-21 17:57:53 -07:00
error_pos_bug2.lean.expected.out	refactor(library): remove unifier_plugin	2016-03-21 17:57:53 -07:00
errors.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
errors.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
errors2.lean	feat(frontends/lean): improve error handling inside match-with expressions	2015-03-13 23:25:46 -07:00
errors2.lean.expected.out	feat(frontends/lean): improve error handling inside match-with expressions	2015-03-13 23:25:46 -07:00
eta_bug.lean	feat(frontends/lean): remove unnecessary option	2015-05-09 11:49:55 -07:00
eta_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
exact_partial.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
exact_partial.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
exact_partial2.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
exact_partial2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
export1.lean	feat(library,frontends/lean/builtin_cmds): store export cmds and replay them	2016-06-03 12:51:12 -07:00
export1.lean.expected.out	feat(library,frontends/lean/builtin_cmds): store export cmds and replay them	2016-06-03 12:51:12 -07:00
focus_tac.lean	feat(library/init/meta/tactic): add 'focus', 'first', 'solve' and LCF-style AND_THEN tactical	2016-06-29 01:07:41 +01:00
focus_tac.lean.expected.out	feat(library/init/meta/tactic): add 'focus' and 'all_goals' tacticals	2016-06-17 16:11:40 -07:00
fold.lean	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
fold.lean.expected.out	fix(tests/lean): adjust tests to reflect changes in the standard library	2015-02-01 11:36:38 -08:00
ftree.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
ftree.lean.expected.out	feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes	2014-11-12 10:52:32 -08:00
gen_as.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
gen_as.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
gen_bug.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
gen_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
goals1.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
goals1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
have1.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
have1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
have_tactic.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
have_tactic.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
ind_parser_bug.lean	fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.	2014-11-05 23:12:00 -08:00
ind_parser_bug.lean.expected.out	fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.	2014-11-05 23:12:00 -08:00
inductive_cmd_leftover_placeholder_universe.lean	fix(frontends/lean/inductive_cmd): remove universe placeholder from parameters	2016-06-14 11:36:34 -07:00
inductive_cmd_leftover_placeholder_universe.lean.expected.out	fix(frontends/lean/inductive_cmd): remove universe placeholder from parameters	2016-06-14 11:36:34 -07:00
inst.lean	feat(frontends/lean/util): remove hack that overrides priority namespace	2015-08-11 18:01:40 -07:00
inst.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
internal_names.lean	fix(frontends/lean): uniform handling of declaration compound names	2016-06-02 18:13:50 -07:00
internal_names.lean.expected.out	fix(frontends/lean): uniform handling of declaration compound names	2016-06-02 18:13:50 -07:00
inv_del.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
inv_del.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
K_bug.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
K_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
let1.lean	feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking	2016-02-29 12:31:23 -08:00
let1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
let3.lean
let3.lean.expected.out
let4.lean
let4.lean.expected.out
lift_coe_off.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
lift_coe_off.lean.expected.out	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
list_monad1.lean	feat(library/init): add 'guard' and helper typeclasses	2016-07-07 00:52:52 -07:00
list_monad1.lean.expected.out	feat(library/init): add 'guard' and helper typeclasses	2016-07-07 00:52:52 -07:00
local_notation_bug.lean	fix(library/scoped_ext): bug in local metadata in sections	2015-04-21 18:56:28 -07:00
local_notation_bug.lean.expected.out	refactor(library): add has_append type class, string concatenation is now an instance of has_append instead of has_add	2016-06-27 08:04:47 +01:00
local_notation_bug2.lean	refactor(library/*): use type classes for div and mod	2015-11-08 14:04:59 -08:00
local_notation_bug2.lean.expected.out	chore(tests/lean): fix tests	2016-06-16 18:47:23 -07:00
match_bug.lean	fix(frontends/lean/decl_cmds): assertion violation	2015-03-25 13:46:23 -07:00
match_bug.lean.expected.out	chore(frontends/lean/decl_cmds): use 'pattern' instead of recursive equation	2016-06-24 16:31:06 -07:00
mismatch.lean	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
mismatch.lean.expected.out	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
namespace_bug.lean	fix(tests/lean): tests affected by new type class resolution procedure	2015-11-08 14:04:58 -08:00
namespace_bug.lean.expected.out	fix(tests/lean): tests affected by new type class resolution procedure	2015-11-08 14:04:58 -08:00
nary_overload.lean	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
nary_overload.lean.expected.out	feat(frontends/lean): allow user to overload notation containing foldr/foldl and/or scoped expressions	2015-08-16 18:24:30 -07:00
nat_pp.lean	fix(tests/lean): adjust some tests to changes in the standard library	2015-11-08 14:04:56 -08:00
nat_pp.lean.expected.out	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
nested1.lean	feat(frontends/lean): allow the user to mark subterms that should be automatically abstracted into new definitions	2015-06-12 17:49:26 -07:00
nested1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
nested2.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
nested2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
no_confusion_type.lean	feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations	2015-02-25 17:00:10 -08:00
no_confusion_type.lean.expected.out	fix(tests/lean): to reflect recent changes	2014-12-01 17:14:11 -08:00
noncomp.lean	feat(library): add 'noncomputable' keyword for the standard library	2015-07-28 21:56:35 -07:00
noncomp.lean.expected.out	feat(library): add 'noncomputable' keyword for the standard library	2015-07-28 21:56:35 -07:00
noncomp_error.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
noncomp_error.lean.expected.out	feat(frontends/lean/decl_cmds): reject unnecessary "noncomputable" annotations	2015-07-29 13:01:07 -07:00
noncomp_hott.hlean	feat(frontends/lean/decl_cmds): sign an error if "noncomputable" keyword is used in the HoTT library or with non-definitions	2015-07-29 13:01:06 -07:00
noncomp_hott.hlean.expected.out	feat(frontends/lean/decl_cmds): sign an error if "noncomputable" keyword is used in the HoTT library or with non-definitions	2015-07-29 13:01:06 -07:00
noncomp_thm.lean	feat(frontends/lean/decl_cmds): sign an error if "noncomputable" keyword is used in the HoTT library or with non-definitions	2015-07-29 13:01:06 -07:00
noncomp_thm.lean.expected.out	feat(frontends/lean/decl_cmds): sign an error if "noncomputable" keyword is used in the HoTT library or with non-definitions	2015-07-29 13:01:06 -07:00
notation.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
notation.lean.expected.out
notation2.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
notation2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
notation3.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
notation3.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
notation4.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
notation4.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
notation5.lean
notation5.lean.expected.out	feat(frontends/lean/notation_cmd): relax restriction on user defined tokens	2016-01-02 13:58:46 -08:00
notation6.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
notation6.lean.expected.out	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
notation7.lean	refactor(library/data/num): break into pieces to reduce dependencies	2014-11-07 08:24:29 -08:00
notation7.lean.expected.out	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
num.lean
num.lean.expected.out	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
num2.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
num2.lean.expected.out
num3.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
num3.lean.expected.out	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
num4.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
num4.lean.expected.out	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
num5.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
num5.lean.expected.out
omit.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
omit.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
open_tst.lean	refactor(*): normalize metaclass names	2015-12-28 10:39:15 -08:00
open_tst.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
param.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
param.lean.expected.out
param_binder_update.lean	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
param_binder_update.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
param_binder_update2.lean	test(tests/lean): add test showing that the binder type update should not change the parameter order	2015-04-22 13:04:05 -07:00
param_binder_update2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
parsing_only.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
parsing_only.lean.expected.out	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
pattern_bug1.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pattern_bug1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pattern_hint1.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pattern_hint1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pattern_pp.lean	feat(frontends/lean/builtin_cmds): show metavariable arguments when pretty printing patterns	2015-12-07 12:39:51 -08:00
pattern_pp.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
place_eqn.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
place_eqn.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pp.lean	feat(frontends/lean): pp.beta is true by default	2015-02-24 12:27:53 -08:00
pp.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pp_algebra_num_bug.lean	fix(frontends/lean): pretty print numeral notation from algebra	2015-03-13 18:58:34 -07:00
pp_algebra_num_bug.lean.expected.out	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
pp_all.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
pp_all.lean.expected.out	fix(library/tc_multigraph): avoid name collisions	2016-02-04 13:15:42 -08:00
pp_all2.lean	feat(frontends/lean/pp): allow user to override pp.all setting	2015-12-11 10:40:48 -08:00
pp_all2.lean.expected.out	feat(frontends/lean/pp): allow user to override pp.all setting	2015-12-11 10:40:48 -08:00
pp_beta.lean	feat(frontends/lean): pp.beta is true by default	2015-02-24 12:27:53 -08:00
pp_beta.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pp_binder_types.lean	feat(frontends/lean/pp): add option to hide binder types	2016-06-02 12:01:57 -07:00
pp_binder_types.lean.expected.out	feat(frontends/lean/pp): add option to hide binder types	2016-06-02 12:01:57 -07:00
pp_bug.lean	fix(frontends/lean/pp): bug in pp arrow	2015-05-31 17:21:37 -07:00
pp_bug.lean.expected.out	fix(frontends/lean/pp): bug in pp arrow	2015-05-31 17:21:37 -07:00
pp_coercions_with_args.lean	fix(src/frontends/lean/pp): pp coercions that take arguments	2016-06-14 11:51:19 -07:00
pp_coercions_with_args.lean.expected.out	fix(src/frontends/lean/pp): pp coercions that take arguments	2016-06-14 11:51:19 -07:00
pp_no_proofs.lean	feat(src/frontends/lean/pp): option to print theorem statements instead of proof terms	2016-06-14 11:50:53 -07:00
pp_no_proofs.lean.expected.out	chore(tests/lean): fix tests output	2016-06-14 11:56:44 -07:00
pp_param_bug.lean	fix(frontends/lean): bug in pretty printer	2015-04-22 12:44:08 -07:00
pp_param_bug.lean.expected.out	fix(frontends/lean): bug in pretty printer	2015-04-22 12:44:08 -07:00
pp_proofs_coercions.lean	feat(src/frontends/lean/pp): look at pp.proofs when pp-ing coercions	2016-06-14 11:51:34 -07:00
pp_proofs_coercions.lean.expected.out	chore(tests/lean): fix tests output	2016-06-17 09:56:57 -07:00
ppbug.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
ppbug.lean.expected.out	chore(tests/lean): fix tests	2016-06-16 18:47:23 -07:00
print_ax1.lean	fix(tests/lean): subtype notation is not in the top-level anymore	2015-12-28 09:04:11 -08:00
print_ax1.lean.expected.out	chore(tests/lean): fix tests output	2016-06-20 11:18:16 -07:00
print_ax2.lean	fix(tests/lean): subtype notation is not in the top-level anymore	2015-12-28 09:04:11 -08:00
print_ax2.lean.expected.out	chore(tests/lean): fix tests output	2016-06-20 11:18:16 -07:00
print_ax3.lean	fix(tests/lean): subtype notation is not in the top-level anymore	2015-12-28 09:04:11 -08:00
print_ax3.lean.expected.out	chore(tests/lean): fix tests output	2016-06-20 11:18:16 -07:00
print_reducible.lean	feat(library/reducible): remove [quasireducible] annotation	2016-02-25 17:42:44 -08:00
print_reducible.lean.expected.out	feat(library/reducible): remove [quasireducible] annotation	2016-02-25 17:42:44 -08:00
print_thm.lean	feat(frontends/lean/builtin_cmds): improve print <id> when <id> is a not yet revealed theorem	2015-06-13 12:12:22 -07:00
print_thm.lean.expected.out	feat(frontends/lean/builtin_cmds): improve print <id> when <id> is a not yet revealed theorem	2015-06-13 12:12:22 -07:00
prodtst.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
prodtst.lean.expected.out	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
protected.lean
protected.lean.expected.out
protected_consts.lean	fix(frontends/lean): consistent behavior for protected declarations	2015-05-18 22:35:18 -07:00
protected_consts.lean.expected.out	feat(frontends/lean): protected constants and axioms	2015-04-19 17:45:58 -07:00
protected_test.lean	feat(nat): redefine le and lt in the standard library	2015-06-04 20:14:13 -04:00
protected_test.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pstate.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
pstate.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
quot_bug.lean	fix(kernel/quotient/quotient): bug in reduction rule	2015-04-29 10:01:17 -07:00
quot_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
quot_ind_bug.lean	fix(kernel/quotient/quotient): bug in reduction rule for quot.ind	2015-05-09 09:07:03 -07:00
quot_ind_bug.lean.expected.out	fix(kernel/quotient/quotient): bug in reduction rule for quot.ind	2015-05-09 09:07:03 -07:00
record_rec_protected.lean	fix(frontends/lean/structure_cmd): 'rec' must be marked as protected	2014-11-03 14:50:12 -08:00
record_rec_protected.lean.expected.out	fix(frontends/lean/structure_cmd): 'rec' must be marked as protected	2014-11-03 14:50:12 -08:00
red.lean	feat(frontends/lean): add '[semireducible]' attribute	2015-03-03 10:48:36 -08:00
red.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
redundant_pattern.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
redundant_pattern.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
replace_tac.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
replace_tac.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
reserve_bugs.lean	fix(tests/lean): adjust some tests to changes in the standard library	2015-11-08 14:04:56 -08:00
reserve_bugs.lean.expected.out	fix(tests/lean): adjust some tests to changes in the standard library	2015-11-08 14:04:56 -08:00
rev_tac1.lean	feat(library/init/meta/tactic): 'revert' tactic returns the number of actually reverted hypothesis	2016-06-28 15:36:50 +01:00
rev_tac1.lean.expected.out	feat(library/init/meta/tactic): 'revert' tactic returns the number of actually reverted hypothesis	2016-06-28 15:36:50 +01:00
rewrite_fail.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
rewrite_fail.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
rewrite_loop.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
rewrite_loop.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
rw_at_failure.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
rw_at_failure.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
rw_set2.lean	feat(frontends/lean,library): rename '[rewrite]' to '[simp]'	2015-07-22 09:01:42 -07:00
rw_set2.lean.expected.out	refactor(simplifier): port skeleton to new tactic framework	2016-06-24 15:20:40 -07:00
sec.lean
sec.lean.expected.out
sec2.lean	refactor(frontends/lean): add 'attribute' command	2015-01-24 20:23:21 -08:00
sec2.lean.expected.out	chore(tests/lean): fix tests output	2016-06-17 09:56:57 -07:00
sec3.lean	chore(tests): remove most occurrences of 'context' command from the test suite	2015-04-21 19:33:21 -07:00
sec3.lean.expected.out	feat(frontends/lean): remove 'context' command	2015-04-22 11:32:02 -07:00
sec_notation2.lean	refactor(library): add has_append type class, string concatenation is now an instance of has_append instead of has_add	2016-06-27 08:04:47 +01:00
sec_notation2.lean.expected.out	refactor(library): add has_append type class, string concatenation is now an instance of has_append instead of has_add	2016-06-27 08:04:47 +01:00
sec_param_pp.lean	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
sec_param_pp.lean.expected.out	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
sec_param_pp2.lean	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
sec_param_pp2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
set_opt_tac.lean	refactor(library/init/meta/tactic): merge trace, trace_fmt and trace_expr	2016-06-23 09:29:42 -07:00
set_opt_tac.lean.expected.out	feat(library/init/meta/tactic,library/tactic/tactic_state): add tactics for setting options	2016-06-18 12:05:58 -07:00
shadow.lean	feat(frontends/lean): ML-like notation for match and recursive equations	2015-02-25 16:20:44 -08:00
shadow.lean.expected.out	feat(frontends/lean): ML-like notation for match and recursive equations	2015-02-25 16:20:44 -08:00
show1.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
show1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
show_tac.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
show_tac.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
showenv.l
simp_idp.hlean	feat(hott/init/path): mark 'idp' and 'idpath' with '[unfold-m]' hint	2015-05-04 14:29:22 -07:00
simp_idp.hlean.expected.out	feat(hott/init/path): mark 'idp' and 'idpath' with '[unfold-m]' hint	2015-05-04 14:29:22 -07:00
simplifier1.hlean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier1.hlean.expected.out	test(tests/lean/simplifier1): add HoTT test for simplifier	2015-11-08 14:05:03 -08:00
simplifier1.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier2.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier3.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier3.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier4.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier4.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier5.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier5.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier6.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier6.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier7.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier7.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier8.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier8.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier9.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier9.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier10.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier10.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier11.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier11.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier12.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier12.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier13.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier13.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier14.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier14.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier15.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier15.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier16.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier16.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier17.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier17.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier18.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier18.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier19.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier19.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier20.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier20.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier21.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier21.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier_norm_num.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier_norm_num.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier_unit_preprocess.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
simplifier_unit_preprocess.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
str1.lean	test(tests/lean): add test for new string support	2016-05-24 16:27:12 -07:00
str1.lean.expected.out	refactor(library): add has_append type class, string concatenation is now an instance of has_append instead of has_add	2016-06-27 08:04:47 +01:00
struct_class.lean	feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used	2014-11-03 17:47:08 -08:00
struct_class.lean.expected.out	feat(library/init): add 'guard' and helper typeclasses	2016-07-07 00:52:52 -07:00
structure_result_type_may_be_zero.lean	fix(src/frontends/lean/structure_cmd): fixes #1036	2016-06-14 17:52:31 -07:00
structure_result_type_may_be_zero.lean.expected.out	fix(src/frontends/lean/structure_cmd): fixes #1036	2016-06-14 17:52:31 -07:00
structure_with_index_error.lean	fix(src/frontends/lean/structure_cmd): check if indices are provided	2016-06-14 17:52:19 -07:00
structure_with_index_error.lean.expected.out	fix(src/frontends/lean/structure_cmd): check if indices are provided	2016-06-14 17:52:19 -07:00
subpp.lean	fix(tests/lean): subtype notation is not in the top-level anymore	2015-12-28 09:04:11 -08:00
subpp.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
subset_error.lean	refactor(logic/funext.lean, algebra/function.lean): delete logic/funext, merge into algebra/function	2015-05-23 16:16:36 +10:00
subset_error.lean.expected.out	feat(frontends/lean/elaborator): include overload information in error messages	2015-05-20 17:21:27 -07:00
subst_bug.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
subst_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
substvars2.hlean	feat(library/tactic): add 'subtvars' tactic	2015-05-25 16:36:44 -07:00
substvars2.hlean.expected.out	feat(library/tactic): add 'subtvars' tactic	2015-05-25 16:36:44 -07:00
t2.lean
t2.lean.expected.out
t3.lean	fix(frontends/lean): uniform handling of declaration compound names	2016-06-02 18:13:50 -07:00
t3.lean.expected.out	fix(frontends/lean): uniform handling of declaration compound names	2016-06-02 18:13:50 -07:00
t5.lean
t5.lean.expected.out	refactor(library): move 'none', 'some', 'tt', 'ff' to top-level	2016-06-25 12:39:19 -07:00
t6.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
t6.lean.expected.out	feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command	2014-10-30 13:12:45 -07:00
t9.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
t9.lean.expected.out	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
t10.lean	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
t10.lean.expected.out	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
t11.lean	fix(tests/lean): adjust tests to reflect changes in the pretty printer	2015-09-30 17:42:07 -07:00
t11.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
t12.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
t12.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
t13.lean	fix(tests/lean): adjust tests to modifications to standard library	2014-11-30 21:16:01 -08:00
t13.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
t14.lean	refactor(*): normalize metaclass names	2015-12-28 10:39:15 -08:00
t14.lean.expected.out
tactic_error_msg.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
tactic_error_msg.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
tactic_failure.lean	feat(library/tactic): store tactic_state at failure	2016-06-13 15:25:55 -07:00
tactic_failure.lean.expected.out	fix(tests/lean): tests	2016-06-14 21:52:52 -07:00
tactic_id_bug.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
tactic_id_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
tactic_var_bug.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
tactic_var_bug.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
test.sh	feat(frontends/lean): apply eta-reduction in postprocessing step	2015-06-10 16:29:30 -07:00
test_single.sh	fix(tests/lean): make sure tests do not fail when compiling Lean with cmake option "-DIGNORE_SORRY=ON"	2015-05-11 11:49:23 -07:00
test_single_pp.sh	fix(test*.sh): allow spaces in filename	2015-03-28 23:29:52 -04:00
trace1.lean	feat(library/init/meta/tactic): add 'when_tracing' tactical	2016-06-28 11:29:39 +01:00
trace1.lean.expected.out	feat(library/init/meta/tactic): add 'when_tracing' tactical	2016-06-28 11:29:39 +01:00
trace2.lean	feat(frontends/lean): add declare_trace command	2016-06-28 11:45:56 +01:00
trace2.lean.expected.out	feat(frontends/lean): add declare_trace command	2016-06-28 11:45:56 +01:00
tuple.lean	test(tests/lean): remove data.nat dependency	2014-12-23 17:42:56 -08:00
tuple.lean.expected.out
unfold.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold_crash.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold_crash.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold_rec2.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold_rec2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold_rec3.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold_rec3.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold_rec4.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfold_rec4.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfoldf.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unfoldf.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
uni_bug1.lean	fix(tests/lean): adjust some tests to changes in the standard library	2015-11-08 14:04:56 -08:00
uni_bug1.lean.expected.out	refactor(library): move 'none', 'some', 'tt', 'ff' to top-level	2016-06-25 12:39:19 -07:00
unification_hints1.lean	feat(library/type_context): unification hints	2016-03-25 16:51:51 -07:00
unification_hints1.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unifier_bug.lean	refactor(library): rename heq.of_eq heq.to_eq auxiliary lemmas	2016-01-09 12:32:18 -08:00
unifier_bug.lean.expected.out	refactor(library): rename heq.of_eq heq.to_eq auxiliary lemmas	2016-01-09 12:32:18 -08:00
unify1.lean	test(tests/lean/run/unify1.lean): new type_context is_def_eq	2016-03-25 17:14:59 -07:00
unify1.lean.expected.out	test(tests/lean/run/unify1.lean): new type_context is_def_eq	2016-03-25 17:14:59 -07:00
unify2.lean	chore(frontends/lean): remove useless elaborator options	2016-04-05 16:03:10 -07:00
unify2.lean.expected.out	chore(frontends/lean): remove useless elaborator options	2016-04-05 16:03:10 -07:00
unify3.lean	refactor(library/init/meta/tactic): merge trace, trace_fmt and trace_expr	2016-06-23 09:29:42 -07:00
unify3.lean.expected.out	feat(library/tactic/tactic_state): add get_assignment and get_univ_assignment	2016-06-18 11:34:00 -07:00
univ.lean	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
univ.lean.expected.out	fix(tests,doc): adjust tests and documentation	2015-11-20 17:03:17 -08:00
univ_vars.lean
univ_vars.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unsolved_proof_qed.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
unsolved_proof_qed.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
user_rec_crash.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
user_rec_crash.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
var.lean	chore(tests): remove most occurrences of 'context' command from the test suite	2015-04-21 19:33:21 -07:00
var.lean.expected.out
var2.lean	chore(tests): remove most occurrences of 'context' command from the test suite	2015-04-21 19:33:21 -07:00
var2.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
whnf.lean	fix(tests/lean): adjust remaining tests to changes in the standard library	2015-11-08 14:04:56 -08:00
whnf.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
with_options.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
with_options.lean.expected.out	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00