max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean
History
Leonardo de Moura 1e6b3614ab feat(frontends/lean): new pattern matching validation 
@Kha, we now support variable/constant shadowing in patterns.
A constant may occur in a pattern if it is a constructor or tagged with
the new [pattern] attribute. In the standard library, I have tagged
'add', 'zero', 'one', 'bit0', 'bit1' and 'rfl' with this new attribute.
BTW, arbitrary constants and variables may occur nested in type ascriptions and
inaccessible terms.

Here is an example:

     meta_definition tactic_result_to_string {A : Type} : tactic_result A → string
     | (success a s)   := to_string a
     | (exception ⌞A⌟ e s) := "Exception: " ++ to_string (e ())

I had to use the inaccessible ⌞A⌟ in the example above, otherwise, we would be shadowing the parameter
{A : Type}, and we would get a type error.

The new validation is performed at to_pattern_fn (parser.cpp).
2016-08-07 11:31:11 -07:00
..
expensive
extra chore(library/init/reserved_notation): add <= and >= 2016-07-09 14:03:05 -07:00
hott refactor(frontends/lean): remove 'by+' and 'begin+' tokens 2016-02-29 13:45:43 -08:00
interactive chore(tests/lean): adjust tests 2016-07-23 12:48:35 -07:00
perf fix(tests/lean/perf): fix tests, simp now invokes 'try triv' 2016-07-17 15:34:20 -04:00
run feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -07:00
slow chore(tests/lean): disable tests 2016-06-10 18:29:41 -07:00
smt2 test(frontends/smt2): basic tests for parser and elaborator 2016-07-29 10:44:44 -07:00
trust0
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
480.hlean.expected.out
487.hlean
487.hlean.expected.out
531.hlean
531.hlean.expected.out
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
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
582.hlean.expected.out
584a.lean
584a.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
584b.lean
584b.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
584c.lean
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
604.lean.expected.out
608.hlean
608.hlean.expected.out
626a.lean feat(frontends/lean/scanner): disallow superscripts in identifiers 2016-01-26 18:46:40 -08:00
626a.lean.expected.out
626b.hlean
626b.hlean.expected.out
626c.lean
626c.lean.expected.out
634.lean
634.lean.expected.out
634b.lean
634b.lean.expected.out
634c.lean
634c.lean.expected.out
634d.lean
634d.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
640.hlean
640.hlean.expected.out
640a.hlean
640a.hlean.expected.out
640b.lean
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
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
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
690.hlean.expected.out
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
712.lean
712.lean.expected.out feat(frontends/lean): quoted names 2016-07-22 19:06:57 -07:00
770.hlean
770.hlean.expected.out
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
778.hlean.expected.out
779.hlean
779.hlean.expected.out
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
858.lean.expected.out feat(frontends/lean/decl_cmds): use new elaborator for variable, parameter and constant commands 2016-08-03 17:10:45 -07:00
893.hlean
893.hlean.expected.out
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
abbrev1.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
abbrev2.lean feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
abbrev2.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
abbrev_paren.hlean
abbrev_paren.hlean.expected.out
acc.lean
acc.lean.expected.out chore(tests/lean): fix tests output 2016-07-26 17:54:30 -07:00
acc_rec_bug.lean
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
anc1.lean feat(frontends/lean/elaborator): chaining for anonymous constructors 2016-08-04 15:08:25 -07:00
anc1.lean.expected.out feat(frontends/lean/elaborator): chaining for anonymous constructors 2016-08-04 15:08:25 -07:00
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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
assert_tac3.lean.expected.out fix(frontends/lean/pp): purify metavar_decl_ref's 2016-07-30 20:30:03 -07:00
auto_include.lean
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
bad_end.lean
bad_end.lean.expected.out
bad_eqns.lean
bad_eqns.lean.expected.out feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -07:00
bad_id.lean
bad_id.lean.expected.out
bad_notation.lean
bad_notation.lean.expected.out
bad_open.lean feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
bad_open.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04: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): new pattern matching validation 2016-08-07 11:31:11 -07:00
bad_print.lean
bad_print.lean.expected.out
bad_quoted_symbol.lean feat(frontends/lean): quoted names 2016-07-22 19:06:57 -07:00
bad_quoted_symbol.lean.expected.out feat(frontends/lean): quoted names 2016-07-22 19:06:57 -07:00
bad_set_option.lean
bad_set_option.lean.expected.out
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
bug1.lean.expected.out chore(tests/lean): fix tests output 2016-07-26 17:54:30 -07:00
by_contradiction.lean fix(library): remove classical instances from global scope 2016-07-29 23:44:23 -04:00
by_contradiction.lean.expected.out fix(library): remove classical instances from global scope 2016-07-29 23:44:23 -04:00
calc1.lean feat(frontends/lean/elaborator): modify the pre-term for overloaded notation 2016-07-31 17:14:01 -07:00
calc1.lean.expected.out feat(frontends/lean/elaborator): modify the pre-term for overloaded notation 2016-07-31 17:14:01 -07:00
cases_failure.hlean
cases_failure.hlean.expected.out
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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
change1.lean.expected.out feat(library/tactic): add 'change' tactic 2016-06-17 13:21:52 -07:00
change2.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -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
char_lits.lean feat(frontends/lean): add support for character literals 2016-07-18 14:07:10 -04:00
char_lits.lean.expected.out feat(frontends/lean): add support for character literals 2016-07-18 14:07:10 -04:00
check.lean
check.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
check2.lean
check2.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -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 feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
cls_err.lean
cls_err.lean.expected.out
coe1.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
coe1.lean.expected.out test(tests/lean/coe1): add coercion tests 2016-07-30 12:29:12 -07:00
coe2.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
coe2.lean.expected.out feat(frontends/lean/pp): add option for hiding coercions 2016-07-30 12:25:18 -07:00
coe3.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
coe3.lean.expected.out fix(library/type_context): bug in type class resolution 2016-07-30 15:54:28 -07:00
coe4.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
coe4.lean.expected.out feat(frontends/lean/elaborator): coercions to functions 2016-07-30 18:54:20 -07:00
coe5.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
coe5.lean.expected.out feat(frontends/lean/elaborator): coercions to functions 2016-07-30 18:54:20 -07:00
coe6.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
coe6.lean.expected.out feat(frontends/lean/elaborator): coercions to sort 2016-07-30 19:47:04 -07:00
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
config.hlean.expected.out
config.lean
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
congr_print.lean.expected.out refactor(simplifier): port skeleton to new tactic framework 2016-06-24 15:20:40 -07:00
const.lean feat(frontends/lean/decl_cmds): use new elaborator for variable, parameter and constant commands 2016-08-03 17:10:45 -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
crash.lean.expected.out chore(library/pp_options): remove option pp.metavar_args 2016-07-31 16:00:21 -07:00
ctx.lean
ctx.lean.expected.out fix(tests/lean): tests 2016-06-14 21:52:52 -07:00
ctxopt.lean
ctxopt.lean.expected.out
defeq1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
defeq1.lean.expected.out feat(library/tactic): add tactic.defeq_simp 2016-06-17 11:20:15 -07:00
defeq_simp1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
defeq_simp2.lean.expected.out chore(tests/lean): fix tests output 2016-07-26 17:54:30 -07:00
defeq_simp_lemmas1.lean feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
defeq_simp_lemmas1.lean.expected.out feat(frontends/lean/pp): improve purify_metavars 2016-07-30 15:31:06 -07:00
defeq_simp_lemmas2.lean feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
defeq_simp_lemmas2.lean.expected.out feat(frontends/lean/pp): improve purify_metavars 2016-07-30 15:31:06 -07:00
elab1.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab1.lean.expected.out feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result 2016-07-27 15:29:25 -07:00
elab2.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab2.lean.expected.out fix(frontends/lean/pp): purify metavar_decl_ref's 2016-07-30 20:30:03 -07:00
elab3.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab3.lean.expected.out chore(tests/lean): fix tests 2016-08-04 19:17:08 -07:00
elab4.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab4.lean.expected.out fix(frontends/lean/elaborator): order type class instances are synthesized 2016-08-01 23:59:22 -07:00
elab4b.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab4b.lean.expected.out fix(frontends/lean/elaborator): order type class instances are synthesized 2016-08-01 23:59:22 -07:00
elab5.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab5.lean.expected.out test(tests/lean): more examples 2016-07-27 16:08:33 -07:00
elab6.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab6.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
elab7.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab7.lean.expected.out feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result 2016-07-27 15:29:25 -07:00
elab8.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab8.lean.expected.out feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result 2016-07-27 15:29:25 -07:00
elab9.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab9.lean.expected.out test(tests/lean): more examples 2016-07-27 16:08:33 -07:00
elab10.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab10.lean.expected.out test(tests/lean/elab10): test show/have-exprs using new elaborator 2016-07-27 16:50:18 -07:00
elab11.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab11.lean.expected.out refactor(frontends/lean/elaborator): snapshots 2016-07-29 10:36:14 -07:00
elab12.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab12.lean.expected.out feat(frontends/lean/elaborator): coercions to functions 2016-07-30 18:54:20 -07:00
elab13.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab13.lean.expected.out fix(frontends/lean/elaborator): check expected type in applications, make sure we don't accidentally unfold definitions unnecessarily 2016-07-28 17:30:56 -07:00
elab14.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab14.lean.expected.out feat(frontends/lean/elaborator): convert unassigned universe levels into universe parameters, basic support for by tactic 2016-07-31 03:45:18 -07:00
elab15.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab15.lean.expected.out feat(frontends/lean/elaborator): invoke tactics 2016-07-31 11:56:52 -07:00
empty.lean
empty.lean.expected.out
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
error_full_names.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
error_loc_bug.lean feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -07:00
error_loc_bug.lean.expected.out feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -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
errors2.lean.expected.out
eta_bug.lean
eta_bug.lean.expected.out refactor(library): remove eq.ops namespace 2016-07-31 12:50:11 -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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
focus_tac.lean.expected.out fix(frontends/lean/pp): purify metavar_decl_ref's 2016-07-30 20:30:03 -07:00
fold.lean
fold.lean.expected.out
format_thunk1.lean feat(library/vm/vm_format,library/tactic): use thunks unit->format when producing error messages 2016-08-04 19:19:09 -07:00
format_thunk1.lean.expected.out feat(library/vm/vm_format,library/tactic): use thunks unit->format when producing error messages 2016-08-04 19:19:09 -07:00
ftree.lean chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
ftree.lean.expected.out chore(tests/lean): fix test output 2016-08-03 14:17:29 -07: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
generalize1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
generalize1.lean.expected.out chore(tests/lean): fix tests output 2016-07-26 17:54:30 -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 refactor(library): remove eq.ops namespace 2016-07-31 12:50:11 -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
hex_char.lean feat(frontends/lean/scanner): hex scape in character literal 2016-07-19 12:38:20 -04:00
hex_char.lean.expected.out feat(frontends/lean/scanner): hex scape in character literal 2016-07-19 12:38:20 -04:00
hex_numeral.lean feat(frontends/lean/scanner): hexadecimal numerals 2016-07-19 13:04:27 -04:00
hex_numeral.lean.expected.out feat(frontends/lean/scanner): hexadecimal numerals 2016-07-19 13:04:27 -04:00
ind_parser_bug.lean
ind_parser_bug.lean.expected.out
induction_tac1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
induction_tac1.lean.expected.out feat(library/tactic/induction_tactic): clear major premise 2016-07-07 07:39:25 -07: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
inst.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
inst_error.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
inst_error.lean.expected.out chore(tests/lean/inst_error.lean.expected.out): fix output 2016-08-02 13:55:08 -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
key_eqv1.lean feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences' 2016-07-16 15:41:32 -04:00
key_eqv1.lean.expected.out feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences' 2016-07-16 15:41:32 -04: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 feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
let3.lean
let3.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
let4.lean
let4.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
lift_coe_off.lean
lift_coe_off.lean.expected.out
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_bug2.lean
local_notation_bug2.lean.expected.out chore(tests/lean): fix tests 2016-06-16 18:47:23 -07:00
match_bug.lean
match_bug.lean.expected.out feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -07:00
mismatch.lean
mismatch.lean.expected.out
namespace_bug.lean
namespace_bug.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
nary_overload.lean
nary_overload.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
nat_pp.lean
nat_pp.lean.expected.out
nested1.lean chore(frontends/lean/nested_declaration): do not allow attributes in abstract ... end blocks 2016-07-31 19:14:33 -07:00
nested1.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04: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): use new elaborator in the inductive command 2016-08-03 13:13:12 -07:00
no_confusion_type.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
noncomp.lean
noncomp.lean.expected.out
noncomp_error.lean
noncomp_error.lean.expected.out
noncomp_hott.hlean
noncomp_hott.hlean.expected.out
noncomp_thm.lean
noncomp_thm.lean.expected.out
notation.lean
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
notation6.lean
notation6.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
notation7.lean
notation7.lean.expected.out
num.lean
num.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
num2.lean feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
num2.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
num3.lean feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
num3.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
num4.lean feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
num4.lean.expected.out
num5.lean feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
num5.lean.expected.out
omit.lean
omit.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
over_notation.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
over_notation.lean.expected.out feat(frontends/lean/elaborator): modify the pre-term for overloaded notation 2016-07-31 17:14:01 -07:00
param.lean
param.lean.expected.out
param_binder_update.lean
param_binder_update.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
param_binder_update2.lean
param_binder_update2.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
parsing_only.lean
parsing_only.lean.expected.out
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
pattern_pp.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04: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
pp.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
pp_algebra_num_bug.lean
pp_algebra_num_bug.lean.expected.out
pp_all.lean
pp_all.lean.expected.out chore(library/class): disable [trans_instance] attribute 2016-07-29 23:28:36 -07:00
pp_all2.lean
pp_all2.lean.expected.out chore(tests/lean/pp_all2): fix test output 2016-07-29 23:35:10 -07:00
pp_beta.lean
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
pp_bug.lean.expected.out
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
pp_param_bug.lean.expected.out
ppbug.lean chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
ppbug.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
print_ax1.lean
print_ax1.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
print_ax2.lean
print_ax2.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
print_ax3.lean
print_ax3.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04: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
print_thm.lean.expected.out
private_structure.lean feat(frontends/lean/structure_cmd): private structures 2016-08-06 00:03:06 -07:00
private_structure.lean.expected.out feat(frontends/lean/structure_cmd): private structures 2016-08-06 00:03:06 -07:00
prodtst.lean
prodtst.lean.expected.out
protected.lean
protected.lean.expected.out
protected_consts.lean
protected_consts.lean.expected.out
protected_test.lean
protected_test.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -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
qexpr1.lean feat(library/tactic, frontends/lean/elaborator): add to_expr tactic 2016-07-31 20:21:17 -07:00
qexpr1.lean.expected.out feat(library/tactic, frontends/lean/elaborator): add to_expr tactic 2016-07-31 20:21:17 -07:00
qexpr2.lean fix(library/tactic/elaborate): new subgoals must be inserted after main goal 2016-07-31 21:16:29 -07:00
qexpr2.lean.expected.out feat(library/tactic/elaborate): convert unassigned metavars into new goals 2016-07-31 20:38:57 -07:00
qexpr3.lean feat(library/init/meta/tactic): add 'refine' tactic 2016-07-31 21:17:19 -07:00
qexpr3.lean.expected.out feat(library/init/meta/tactic): add 'refine' tactic 2016-07-31 21:17:19 -07:00
quot_bug.lean
quot_bug.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
quot_ind_bug.lean
quot_ind_bug.lean.expected.out
record_rec_protected.lean chore(tests/lean): fix tests 2016-07-07 07:39:26 -07:00
record_rec_protected.lean.expected.out
red.lean
red.lean.expected.out chore(library/pp_options): remove option pp.metavar_args 2016-07-31 16:00:21 -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 feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
reserve_bugs.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
restrict_bug.lean feat(library/type_context): restrict context of metavariables during unification if approximate() is true 2016-08-02 16:31:12 -07:00
restrict_bug.lean.expected.out feat(library/type_context): restrict context of metavariables during unification if approximate() is true 2016-08-02 16:31:12 -07:00
rev_tac1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
rev_tac1.lean.expected.out chore(tests/lean): fix tests output 2016-07-26 17:54:30 -07:00
rewrite1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
rewrite1.lean.expected.out fix(tests/lean/rewrite1): add repeat 2016-07-17 18:19:42 -04: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
rquote.lean feat(frontends/lean): resolved quoted names 2016-08-05 17:04:36 -07:00
rquote.lean.expected.out feat(frontends/lean): resolved quoted names 2016-08-05 17:04:36 -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(simplifier/simp_lemmas): take arbitrary list of attributes and cache 2016-08-03 18:04:28 -07:00
rw_set2.lean.expected.out feat(simplifier/simp_lemmas): take arbitrary list of attributes and cache 2016-08-03 18:04:28 -07:00
sec.lean
sec.lean.expected.out
sec3.lean
sec3.lean.expected.out
sec_param_pp.lean
sec_param_pp.lean.expected.out
sec_param_pp2.lean
sec_param_pp2.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
set_opt_tac.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -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
shadow.lean.expected.out feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -07:00
show1.lean refactor(library): remove eq.ops namespace 2016-07-31 12:50:11 -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
simp_idp.hlean.expected.out
simplifier1.hlean chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
simplifier1.hlean.expected.out
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
struct_class.lean
struct_class.lean.expected.out refactor(library/init/meta): qexpr ==> pexpr 2016-08-05 17:04:36 -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 chore(tests/lean): adjust tests 2016-07-23 12:48:35 -07:00
subpp.lean.expected.out chore(tests/lean): adjust tests 2016-07-23 12:48:35 -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
substvars2.hlean.expected.out
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 feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
t6.lean
t6.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
t10.lean
t10.lean.expected.out
t11.lean
t11.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
t12.lean
t12.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
t13.lean
t13.lean.expected.out feat(frontends/lean/elaborator): modify the pre-term for overloaded notation 2016-07-31 17:14:01 -07:00
t14.lean feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
t14.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -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
test_single.sh
test_single_pp.sh
trace1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
trace1.lean.expected.out feat(library/init/meta/tactic): add 'when_tracing' tactical 2016-06-28 11:29:39 +01:00
trace2.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
trace2.lean.expected.out feat(frontends/lean): add declare_trace command 2016-06-28 11:45:56 +01:00
tuple.lean
tuple.lean.expected.out
type_class_bug.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
type_class_bug.lean.expected.out fix(library/metavar_util): but in instantiate_mvars 2016-08-02 13:16:17 -07:00
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
unfold1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
unfold1.lean.expected.out feat(library/tactic): add unfold tactic 2016-07-18 15:46:56 -04:00
unfold2.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
unfold2.lean.expected.out feat(library/tactic): add unfold tactic 2016-07-18 15:46:56 -04:00
unfold3.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
unfold3.lean.expected.out feat(library/tactic): add unfold tactic 2016-07-18 15:46:56 -04:00
unfold4.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
unfold4.lean.expected.out fix(library/tactic/unfold_tactic): should use type_context locals 2016-07-18 19:08:31 -04:00
unfold_crash.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
unfold_crash.lean.expected.out fix(library/tactic/unfold_crash): crash when constant is not a definition 2016-07-18 19:59:17 -04:00
unfold_crash2.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
unfold_crash2.lean.expected.out feat(library/tactic/unfold_tactic): improve fold failure detection 2016-07-18 20:17:40 -04:00
unfold_fact.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
unfold_fact.lean.expected.out fix(library/tactic/unfold_tactic): should use type_context locals 2016-07-18 19:08:31 -04: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
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(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
unification_hints1.lean.expected.out feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
unifier_bug.lean
unifier_bug.lean.expected.out
unify3.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
unify3.lean.expected.out fix(frontends/lean/pp): purify metavar_decl_ref's 2016-07-30 20:30:03 -07:00
univ.lean
univ.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
univ_vars.lean
univ_vars.lean.expected.out feat(frontends/lean/elaborator): universe parameter name sanitizer 2016-08-03 13:13:44 -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
utf8.lean feat(library/init/string): add utf8_length 2016-07-19 14:22:37 -04:00
utf8.lean.expected.out feat(library/init/string): add utf8_length 2016-07-19 14:22:37 -04:00
var.lean
var.lean.expected.out
var2.lean
var2.lean.expected.out chore(tests/lean): fix/disable tests 2016-06-10 18:29:41 -07:00
vm_eval_crash.lean fix(frontends/lean/builtin_cmds): fail if expression contain metavars 2016-07-19 13:22:10 -04:00
vm_eval_crash.lean.expected.out feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07:00
whnf.lean feat(frontends/lean): use new elaborator in the 'check' command 2016-08-02 14:57:49 -07: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