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 7ebf16ca26 fix(library/equations_compiler): performance issues at structural_rec module and equational lemma generator 
There were two performance bottlenecks in the recursive equation
compiler. Both bottlenecks were due to conversion checking.

1- We allow patterns such as (x+1) in the left-hand-side of a
   recursive equation. This is kind of pattern has to be reduced
   since it is not a constructor. Moreover, when we are trying to
   compile using structural recursion, we need to find an element
   that is structurally smaller in recursive applications.
   Again, we need to use reduction since the pattern may be (x+2),
   and in the recursive application we have (x+1). Now, consider
   the following equation

         f (x+1) (y+1) := f complex_term y

   It will first check whether complex_term is structurally smaller
   than (x+1), and the compiler will timeout trying to reduce
   complex_term.

   This commit adds the following workaround. The structural
   recursion module from now on will only unfold reducible constants
   and constants marked as patterns. This is not a complete
   solution. It will timeout in the following equation:

         f (x+1) (y+1) := f (x+1000000000000) y

   For this one, we need to add a whnf "fuel" option to type_context

2- Equational lemma generation was producing lemmas that are too
   expensive to check. Suppose we the following two definitions

       | f x 0     := 1
       | f x (y+1) := f complex_term y

    and

       | g 0     y    := 1
       | g (x+1) y    := g x complex_term

    Before this commit, we would generate the following proofs for
    the second equation of each definition:

         eq.refl (f complex_term y)
         eq.refl (g x complex_term)

    This proof triggers the following definitionally equality test:

             f x     (y+1)  =?= f complex_term y
             g (x+1) y      =?= g x complex_term

    Since, we have f/g on both sides, the type checker will try
    first to unify the arguments, and may timeout trying to solve

               x  =?= complex_term
               y  =?= complex_term

    since it may take a long time to reduce `complex_term`.

    We workaround this problem by creating a slightly different
    proof.

          eq.refl (unfold_of(f x (y+1)))
          eq.refl (unfold_of(g (x+1) y))

    where unfold_of(t) is the result of applying one delta reduction
    step.
2017-02-15 21:31:28 -08:00
..
extra chore(frontends/lean): new_elaborator is now the default 2016-09-19 16:34:06 -07:00
fail feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -08:00
interactive refactor(library/init/meta): remove whnf_core 2017-02-14 18:39:57 -08:00
native_run feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
perf
run fix(library/equations_compiler): performance issues at structural_rec module and equational lemma generator 2017-02-15 21:31:28 -08:00
server fix(frontends/lean/parser): crash on Win 10 2016-11-07 21:30:19 -08:00
slow
smt2
trust0 feat(tests): run tests in emscripten build 2016-10-16 14:41:35 -07:00
trust10 feat(tests): run tests in emscripten build 2016-10-16 14:41:35 -07:00
584a.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
584a.lean.expected.out chore(frontends/lean/print_cmd): update print command to keyword changes 2017-01-12 12:04:37 -08:00
584b.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
584b.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
584c.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
584c.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
634.lean fix(frontends/lean/pp): pretty print issue, and fix broken tests output 2016-12-15 15:42:54 -08:00
634.lean.expected.out fix(frontends/lean/pp): pretty print issue, and fix broken tests output 2016-12-15 15:42:54 -08:00
634b.lean fix(frontends/lean/pp): pretty print issue, and fix broken tests output 2016-12-15 15:42:54 -08:00
634b.lean.expected.out fix(frontends/lean/pp): pretty print issue, and fix broken tests output 2016-12-15 15:42:54 -08:00
634c.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
634c.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
634d.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
634d.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
652.lean
652.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
671.lean
671.lean.expected.out fix(library/equations_compiler): performance issues at structural_rec module and equational lemma generator 2017-02-15 21:31:28 -08:00
712.lean
712.lean.expected.out
858.lean
858.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
1162.lean feat(library/equations_compiler/elim_match): report unused equations 2016-10-19 09:58:08 -07:00
1162.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
1207.lean feat(tests/lean/1207): add the other example used in the issue #1207 2016-12-01 17:18:41 -08:00
1207.lean.expected.out fix(frontends/lean/tactic_notation): fixes #1207 2016-12-01 17:16:22 -08:00
1258.lean fix(library/type_context): issue #1258 again 2016-12-22 10:51:16 -08:00
1258.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
1277.lean chore(tests/lean/1277): remove trace 2017-01-23 18:40:22 -08:00
1277.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
1279.lean fix(frontends/lean/elaborator): cactch app_exception when trying to create coercion 2017-01-03 09:03:00 -08:00
1279.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
1290.lean fix(frontends/lean/parser): fixes #1290 2017-01-09 15:35:25 -08:00
1290.lean.expected.out fix(frontends/lean/parser): fixes #1290 2017-01-09 15:35:25 -08:00
1292.lean fix(frontends/lean): fixes #1292 2017-01-09 15:53:37 -08:00
1292.lean.expected.out fix(frontends/lean): fixes #1292 2017-01-09 15:53:37 -08:00
1293.lean fix(library/tactic/tactic_state): closes #1293 2017-01-09 16:23:02 -08:00
1293.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
1299.lean fix(frontends/lean/definition_cmds): fix #1299 2017-01-10 14:38:46 -08:00
1299.lean.expected.out chore(frontends/lean/print_cmd): update print command to keyword changes 2017-01-12 12:04:37 -08:00
1327.lean fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching 2017-01-21 22:38:17 -08:00
1327.lean.expected.out fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching 2017-01-21 22:38:17 -08:00
1369.lean fix(library/tactic): fixes #1369 2017-02-10 15:58:27 -08:00
1369.lean.expected.out fix(library/tactic): fixes #1369 2017-02-10 15:58:27 -08:00
alias.lean chore(frontends/lean): remove dead code from parser 2016-09-19 17:04:59 -07:00
alias.lean.expected.out
alias2.lean
alias2.lean.expected.out
anc1.lean chore(library/init): adjust Sort vs Type in definitions 2017-01-30 12:50:18 -08:00
anc1.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
assert_tac3.lean
assert_tac3.lean.expected.out chore(frontends/lean/print_cmd): update print command to keyword changes 2017-01-12 12:04:37 -08:00
assumption_tac_notation.lean feat(library/tactic): add back notation for by assumption 2016-10-11 14:17:18 -07:00
assumption_tac_notation.lean.expected.out feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
attribute_bug1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
attribute_bug1.lean.expected.out chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
attributes.lean feat(frontends/lean): anonymous instances 2016-09-23 13:34:34 -07:00
attributes.lean.expected.out chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
auto_quote_error.lean feat(frontends/lean,library/tactic/tactic_state): improve error localization 2016-09-25 18:40:41 -07:00
auto_quote_error.lean.expected.out fix(frontends/lean, library/tactic): error position in auto quoted terms 2017-02-09 18:03:04 -08:00
auto_quote_error2.lean feat(frontends/lean): add step-by-step 'begin...end' block execution 2016-09-26 10:56:40 -07:00
auto_quote_error2.lean.expected.out fix(frontends/lean, library/tactic): error position in auto quoted terms 2017-02-09 18:03:04 -08:00
aux_decl_zeta.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
aux_decl_zeta.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
bad_end.lean
bad_end.lean.expected.out fix(frontends/lean): bad position at spurious 'end' token 2016-12-29 19:51:36 -08:00
bad_end_error_pos.lean fix(frontends/lean): bad position at spurious 'end' token 2016-12-29 19:51:36 -08:00
bad_end_error_pos.lean.expected.out fix(frontends/lean): bad position at spurious 'end' token 2016-12-29 19:51:36 -08:00
bad_error1.lean fix(frontends/lean/elaborator): bad error message 2016-11-21 12:18:31 -08:00
bad_error1.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
bad_error2.lean refactor(library/init/data/nat/basic,lemmas): alternative name, and rename le.elim to le.dest 2016-12-08 07:20:02 -08:00
bad_error2.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
bad_error3.lean feat(frontends/lean/elaborator): catch error early 2017-01-05 13:37:55 -08:00
bad_error3.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
bad_error4.lean feat(frontends/lean/elaborator): catch exception at is_def_eq 2017-01-06 08:16:51 -08:00
bad_error4.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
bad_error5.lean fix(frontends/lean/tactic_evaluator): show VM errors on tactic 2017-01-10 14:42:48 -08:00
bad_error5.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
bad_id.lean
bad_id.lean.expected.out chore(tests/lean): make sure all tests can be processed using new elaborator 2016-09-19 16:17:32 -07:00
bad_inaccessible.lean feat(frontends/lean/definition_cmds): improve error minimization 2016-09-23 10:16:46 -07:00
bad_inaccessible.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
bad_inaccessible2.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
bad_inaccessible2.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
bad_index.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
bad_index.lean.expected.out fix(kernel/inductive/inductive): kernel should reject inductive datatype declaration for I where I occurs in an index 2016-09-10 17:45:58 -07:00
bad_notation.lean
bad_notation.lean.expected.out
bad_open.lean
bad_open.lean.expected.out
bad_pattern2.lean
bad_pattern2.lean.expected.out fix(frontends/lean/parser): support as_atomic exprs at to_pattern_fn 2016-09-18 16:55:59 -07:00
bad_print.lean
bad_print.lean.expected.out
bad_quoted_symbol.lean
bad_quoted_symbol.lean.expected.out
bad_set_option.lean
bad_set_option.lean.expected.out
bad_structures.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
bad_structures.lean.expected.out fix(frontends/lean/structure_cmd): handle is_one_placeholder 2016-10-02 08:07:19 -07:00
bad_structures2.lean
bad_structures2.lean.expected.out
begin_end_bug.lean fix(frontends/lean): begin...end block scope 2017-01-03 21:01:14 -08:00
begin_end_bug.lean.expected.out fix(frontends/lean): begin...end block scope 2017-01-03 21:01:14 -08:00
bug1.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
bug1.lean.expected.out fix(frontends/lean): 'sorry' axiom auto generation 2016-12-08 10:31:52 -08:00
by_contradiction.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
by_contradiction.lean.expected.out chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
caching_user_attribute.lean feat(library/init/meta/attribute, library/tactic/user_attribute): make sure caching_user_attribute is in (Type 1) 2016-10-04 02:05:34 -07:00
caching_user_attribute.lean.expected.out fix(library/tactic/user_attribute): make sure it compiles when using older versions of g++ 2016-09-12 10:51:25 -07:00
calc1.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
calc1.lean.expected.out
change1.lean chore(tests/lean): get tests working again 2016-11-29 11:12:44 -08:00
change1.lean.expected.out
change2.lean chore(tests/lean): get tests working again 2016-11-29 11:12:44 -08:00
change2.lean.expected.out
char_lits.lean feat(frontends/lean): use #"c" instead of 'c' for character literals 2016-11-17 11:35:54 -08:00
char_lits.lean.expected.out feat(frontends/lean): use #"c" instead of 'c' for character literals 2016-11-17 11:35:54 -08:00
check.lean
check.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
check2.lean
check2.lean.expected.out
choice_expl.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
choice_expl.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
cls_err.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
cls_err.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
coe1.lean chore(tests/lean): fix tests 2016-12-15 17:04:21 -08:00
coe1.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
coe2.lean chore(tests/lean): fix tests 2016-12-15 17:04:21 -08:00
coe2.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
coe3.lean feat(library/init/coe): add coercion from A to (option A) 2017-01-31 17:45:41 -08:00
coe3.lean.expected.out
coe4.lean feat(library/init/coe,frontends/lean): more general coercions to fun 2016-09-27 15:41:06 -07:00
coe4.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
coe5.lean feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class 2016-09-29 17:56:35 -07:00
coe5.lean.expected.out
coe6.lean feat(library/init/coe,frontends/lean): more general coercions to fun 2016-09-27 15:41:06 -07:00
coe6.lean.expected.out feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
combinators1.lean
combinators1.lean.expected.out feat(library/tactic/intro_tactic): use get_unused_name 2016-09-19 16:38:03 -07:00
concrete_instance.lean refactor(library/nat): rename nat.le to nat.less_than 2016-11-25 18:53:03 -08:00
concrete_instance.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
const.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
const.lean.expected.out
crash.lean feat(frontends/lean/definition_cmds): improve error minimization 2016-09-23 10:16:46 -07:00
crash.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
ctx.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
ctx.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
ctx_error_msgs.lean fix(tests/lean/ctx_error_msgs): avoid internal ids 2016-09-28 20:54:10 -07:00
ctx_error_msgs.lean.expected.out chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
ctxopt.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
ctxopt.lean.expected.out
curly_notation.lean feat(frontends/lean): use #"c" instead of 'c' for character literals 2016-11-17 11:35:54 -08:00
curly_notation.lean.expected.out chore(frontends/lean/print_cmd): update print command to keyword changes 2017-01-12 12:04:37 -08:00
def1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def1.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
def2.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
def2.lean.expected.out feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
def3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def3.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
def4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def4.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
def_inaccessible_issue.lean feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08:00
def_inaccessible_issue.lean.expected.out feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08:00
def_ite_value.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_ite_value.lean.expected.out fix(library/tactic/induction_tactic): normalize type in the induction tactic 2016-09-04 17:36:26 -07:00
defeq1.lean chore(tests/lean): get tests working again 2016-11-29 11:12:44 -08:00
defeq1.lean.expected.out
defeq_simp1.lean fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching 2017-01-21 22:38:17 -08:00
defeq_simp1.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
defeq_simp2.lean fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify 2016-10-12 08:33:40 -07:00
defeq_simp2.lean.expected.out fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify 2016-10-12 08:33:40 -07:00
defeq_simp3.lean feat(library/init/meta): rename rsimp* back to dsimp* 2016-10-11 16:37:08 -07:00
defeq_simp3.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
defeq_simp4.lean feat(library/init/meta): rename rsimp* back to dsimp* 2016-10-11 16:37:08 -07:00
defeq_simp4.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
defeq_simp5.lean feat(library/init/meta): rename rsimp* back to dsimp* 2016-10-11 16:37:08 -07:00
defeq_simp5.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
dep_bug.lean
dep_bug.lean.expected.out
do_match_fail.lean feat(frontends/lean): add support for monad_fail type class in 'do' blocks 2017-02-05 20:09:08 -08:00
do_match_fail.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
dsimp_whnf.lean fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify 2016-10-12 08:33:40 -07:00
dsimp_whnf.lean.expected.out fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify 2016-10-12 08:33:40 -07:00
dsimp_whnf_post.lean fix(tactic/dsimplify.cpp): must whnf in post to be idempotent 2016-12-08 13:34:32 -08:00
dsimp_whnf_post.lean.expected.out fix(tactic/dsimplify.cpp): must whnf in post to be idempotent 2016-12-08 13:34:32 -08:00
dunfold_constant.lean fix(init/meta/expr.lean): is_app_of can return true for constants as well 2016-12-08 11:23:53 -08:00
dunfold_constant.lean.expected.out chore(tests/lean/dunfold_constant): fix test output 2016-12-08 11:34:08 -08:00
elab1.lean
elab1.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
elab2.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
elab2.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
elab3.lean
elab3.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
elab4.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
elab4.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
elab4b.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
elab4b.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
elab5.lean
elab5.lean.expected.out
elab6.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
elab6.lean.expected.out chore(library/init): adjust Sort vs Type in definitions 2017-01-30 12:50:18 -08:00
elab7.lean
elab7.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
elab8.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
elab8.lean.expected.out feat(frontends/lean): lambda+anonymous_constructor+match notation 2016-09-21 08:49:05 -07:00
elab9.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
elab9.lean.expected.out feat(frontends/lean): anonymous instances 2016-09-23 13:34:34 -07:00
elab11.lean
elab11.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
elab12.lean
elab12.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
elab13.lean
elab13.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
elab14.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
elab14.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
elab15.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
elab15.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
elab_error_msgs.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
elab_error_msgs.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
elab_error_recovery.lean feat(frontends/lean/elaborator): recover from most errors using sorry 2017-02-06 15:15:44 +01:00
elab_error_recovery.lean.expected.out fix(frontends/lean, library/tactic): error position in auto quoted terms 2017-02-09 18:03:04 -08:00
elab_meta2.lean fix(frontends/lean/pp): pretty print issue, and fix broken tests output 2016-12-15 15:42:54 -08:00
elab_meta2.lean.expected.out feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
empty.lean
empty.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
emptyc_errors.lean feat(library/type_context): solve ?m s =?= ?m t by first-order unification in approximate mode 2016-10-07 12:06:22 -07:00
emptyc_errors.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
eqn_compiler_error_msg.lean feat(frontends/lean/elaborator): add pattern validator in the elaborator 2017-02-04 19:00:20 -08:00
eqn_compiler_error_msg.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
eqn_compiler_loop.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eqn_compiler_loop.lean.expected.out fix(frontends/lean): 'sorry' axiom auto generation 2016-12-08 10:31:52 -08:00
eqn_hole.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eqn_hole.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
error_full_names.lean
error_full_names.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
error_pos.lean fix(frontends/lean): error localization bugs 2016-10-15 13:40:57 -07:00
error_pos.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
errors2.lean
errors2.lean.expected.out
eta_bug.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
eta_bug.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
eta_tac.lean feat(library/init/meta/tactic): add eta reduction tactic 2017-01-06 19:56:10 -08:00
eta_tac.lean.expected.out feat(library/init/meta/tactic): add eta reduction tactic 2017-01-06 19:56:10 -08:00
eval_expr_error.lean feat(library/tactic/eval): eval_expr for arbitrary expressions 2016-10-03 19:01:22 -07:00
eval_expr_error.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
exact_error_pos.lean fix(frontends/lean, library/tactic): error position in auto quoted terms 2017-02-09 18:03:04 -08:00
exact_error_pos.lean.expected.out fix(frontends/lean, library/tactic): error position in auto quoted terms 2017-02-09 18:03:04 -08:00
example_false.lean fix(frontends/lean): type check examples 2016-09-27 14:39:55 -07:00
example_false.lean.expected.out feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
field_access.lean feat(frontends/lean): generalize '~>' notation, and add alias '^.' for '~>' 2016-09-23 08:18:19 -07:00
field_access.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
focus_tac.lean
focus_tac.lean.expected.out chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
fold.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
fold.lean.expected.out
format_thunk1.lean
format_thunk1.lean.expected.out chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
ftree.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
ftree.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
generalize1.lean
generalize1.lean.expected.out
hex_char.lean feat(frontends/lean): use #"c" instead of 'c' for character literals 2016-11-17 11:35:54 -08:00
hex_char.lean.expected.out feat(frontends/lean): use #"c" instead of 'c' for character literals 2016-11-17 11:35:54 -08:00
hex_numeral.lean
hex_numeral.lean.expected.out
hinst_lemmas1.lean feat(library/tactic/smt/hinst_lemmas): change how transparency is used to process hinst_lemmas 2017-01-04 19:12:37 -08:00
hinst_lemmas1.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
hinst_lemmas2.lean feat(library/init/meta/smt/ematch): add commands for creating attributes for hinst_lemmas 2017-01-04 20:31:38 -08:00
hinst_lemmas2.lean.expected.out feat(library/init/meta/smt/ematch): add commands for creating attributes for hinst_lemmas 2017-01-04 20:31:38 -08:00
hole_in_fn.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
hole_in_fn.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
hole_issue2.lean feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's 2017-01-24 15:59:38 -08:00
hole_issue2.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
import_invalid_tk.lean feat(frontends/lean/parser): gracefully handle scanner exceptions in imports 2017-01-11 23:49:44 -08:00
import_invalid_tk.lean.expected.out chore(library/data): rename tuple => vector 2017-01-26 22:11:10 -08:00
import_middle.lean feat(frontends/lean/builtin_cmds): improve error message when import is used in the middle of the file 2017-01-11 11:15:29 -08:00
import_middle.lean.expected.out feat(frontends/lean/builtin_cmds): improve error message when import is used in the middle of the file 2017-01-11 11:15:29 -08:00
inaccessible.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
inaccessible.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
inaccessible2.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
inaccessible2.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
induction_tac1.lean refactor(library/init/meta): avoid '_core' idiom using default parameters 2017-02-14 09:46:55 -08:00
induction_tac1.lean.expected.out chore(tests/lean/induction_tac1): adjust output 2016-10-05 22:01:16 -07:00
inductive_cmd_leftover_placeholder_universe.lean
inductive_cmd_leftover_placeholder_universe.lean.expected.out feat(src/library/inductive_compiler): support for nested inductive types 2016-09-16 12:50:59 -07:00
inline_issue.lean fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied 2017-01-17 16:33:19 -08:00
inline_issue.lean.expected.out fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied 2017-01-17 16:33:19 -08:00
inst.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
inst.lean.expected.out feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
inst_error.lean
inst_error.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
instance_cache1.lean feat(frontends/lean/definition_cmds): improve error minimization 2016-09-23 10:16:46 -07:00
instance_cache1.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
instance_cache_bug1.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
instance_cache_bug1.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
int_eval.lean feat(library/vm): use native representation for int in the VM 2016-12-18 15:04:02 -08:00
int_eval.lean.expected.out feat(library/vm): use native representation for int in the VM 2016-12-18 15:04:02 -08:00
internal_names.lean
internal_names.lean.expected.out
io_bug1.lean fix(library/compiler/erase_irrelevant): make sure io monad actions are not erased by dead code elimination optimization 2017-01-02 01:42:36 -08:00
io_bug1.lean.expected.out fix(library/compiler/erase_irrelevant): make sure io monad actions are not erased by dead code elimination optimization 2017-01-02 01:42:36 -08:00
io_bug2.lean fix(library/compiler/erase_irrelevant): remove broken io monad optimization 2017-02-07 21:24:31 -08:00
io_bug2.lean.expected.out fix(library/compiler/erase_irrelevant): remove broken io monad optimization 2017-02-07 21:24:31 -08:00
key_eqv1.lean
key_eqv1.lean.expected.out fix(tests): update to name hashing changes 2016-10-16 14:41:35 -07:00
let1.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
let1.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
let3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
let3.lean.expected.out feat(frontends/lean/elaborator): switch to new let-decls 2016-09-10 13:00:53 -07:00
let4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
let4.lean.expected.out feat(frontends/lean/elaborator): switch to new let-decls 2016-09-10 13:00:53 -07:00
let_elim_issue.lean fix(library/compiler/erase_irrelevant): issue created by elim_unused_lets optimization 2016-12-14 18:51:53 -08:00
let_elim_issue.lean.expected.out fix(library/compiler/erase_irrelevant): issue created by elim_unused_lets optimization 2016-12-14 18:51:53 -08:00
lift_coe_off.lean
lift_coe_off.lean.expected.out
list_monad1.lean
list_monad1.lean.expected.out
local_notation_bug2.lean
local_notation_bug2.lean.expected.out
local_ref_bugs.lean fix(frontends/lean/elaborator): another issue at resolve_names 2016-12-15 15:11:24 -08:00
local_ref_bugs.lean.expected.out fix(frontends/lean/pp): pretty print issue, and fix broken tests output 2016-12-15 15:42:54 -08:00
match_bug.lean
match_bug.lean.expected.out
minimize_errors.lean feat(frontends/lean): minimize errors being reported 2016-09-23 09:20:31 -07:00
minimize_errors.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
mismatch.lean
mismatch.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
missing_import.lean fix(module_mgr): guard all accesses to m_mod_info 2016-12-23 18:01:44 +01:00
missing_import.lean.expected.out chore(library/data): rename tuple => vector 2017-01-26 22:11:10 -08:00
namespace_bug.lean
namespace_bug.lean.expected.out
nary_overload.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
nary_overload.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
nat_add_assoc_no_axioms.lean feat(tests/lean): add test to make sure simplifier did not introduce unwanted propext 2017-01-20 20:28:49 -08:00
nat_add_assoc_no_axioms.lean.expected.out feat(tests/lean): add test to make sure simplifier did not introduce unwanted propext 2017-01-20 20:28:49 -08:00
nat_pp.lean
nat_pp.lean.expected.out
nested_errors.lean fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place 2017-02-05 18:20:10 -08:00
nested_errors.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
no_confusion_type.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
no_confusion_type.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
no_meta_rec_inst.lean feat(library/type_context): avoid auxiliary definitions introduced by the equation compiler from being used in the type class resolution procedure 2017-02-04 15:56:54 -08:00
no_meta_rec_inst.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
non_exhaustive_error.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
non_exhaustive_error.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
noncomp.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
noncomp.lean.expected.out feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
noncomp_error.lean
noncomp_error.lean.expected.out feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
noncomp_thm.lean
noncomp_thm.lean.expected.out feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
notation.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
notation.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
notation2.lean
notation2.lean.expected.out
notation3.lean
notation3.lean.expected.out
notation4.lean chore(library/init): adjust Sort vs Type in definitions 2017-01-30 12:50:18 -08:00
notation4.lean.expected.out chore(library/init): adjust Sort vs Type in definitions 2017-01-30 12:50:18 -08:00
notation5.lean
notation5.lean.expected.out
notation6.lean
notation6.lean.expected.out
notation7.lean
notation7.lean.expected.out
notation8.lean chore(library/init/function): make '$' right assoc like Haskell 2016-10-02 07:25:50 -07:00
notation8.lean.expected.out
notation_error_pos.lean fix(frontends/lean/parser): position info when error is inside notation 2017-01-16 10:29:00 -08:00
notation_error_pos.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
num.lean
num.lean.expected.out
num2.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
num2.lean.expected.out fix(frontends/lean, library/tactic): error position in auto quoted terms 2017-02-09 18:03:04 -08:00
num3.lean
num3.lean.expected.out fix(frontends/lean, library/tactic): error position in auto quoted terms 2017-02-09 18:03:04 -08:00
num4.lean
num4.lean.expected.out
num5.lean
num5.lean.expected.out
offset_is_def_eq_trick.lean feat(library/type_context): improve offset trick in the unifier 2017-02-04 17:15:05 -08:00
offset_is_def_eq_trick.lean.expected.out feat(library/equations_compiler/util): make sure "inaccessible annotations" do not leak into the type of automatically generated equational lemmas 2017-02-04 17:19:42 -08:00
omit.lean
omit.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
open_namespaces.lean chore(library/scoped_ext,tests/lean): fix issues raised by @kha 2016-12-19 10:03:16 -08:00
open_namespaces.lean.expected.out chore(library/scoped_ext,tests/lean): fix issues raised by @kha 2016-12-19 10:03:16 -08:00
over_notation.lean
over_notation.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
param.lean chore(tests/lean): make sure all tests can be processed using new elaborator 2016-09-19 16:17:32 -07:00
param.lean.expected.out chore(tests/lean): make sure all tests can be processed using new elaborator 2016-09-19 16:17:32 -07:00
param_binder_update.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
param_binder_update.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
param_binder_update2.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
param_binder_update2.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
parsing_only.lean
parsing_only.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
pp.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
pp.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
pp_all.lean refactor(*): remove abbreviation command 2016-09-03 17:11:29 -07:00
pp_all.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
pp_all2.lean
pp_all2.lean.expected.out feat(frontends/lean): anonymous instances 2016-09-23 13:34:34 -07:00
pp_beta.lean chore(tests/lean): adjust tests to recent changes 2017-01-20 19:08:41 -08:00
pp_beta.lean.expected.out chore(tests/lean): adjust tests to recent changes 2017-01-20 19:08:41 -08:00
pp_binder_types.lean
pp_binder_types.lean.expected.out chore(frontends/lean/print_cmd): update print command to keyword changes 2017-01-12 12:04:37 -08:00
pp_bug.lean
pp_bug.lean.expected.out
pp_char_bug.lean fix(library/string,library/init/data/to_string): handle ASCII control characters 2017-01-11 23:44:33 -08:00
pp_char_bug.lean.expected.out feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
pp_goal_issue.lean fix(library/tactic/tactic_state): goal pp problem reported by Jared 2016-12-19 20:32:44 -08:00
pp_goal_issue.lean.expected.out fix(library/tactic/tactic_state): goal pp problem reported by Jared 2016-12-19 20:32:44 -08:00
pp_no_proofs.lean feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
pp_no_proofs.lean.expected.out feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
pp_param_bug.lean
pp_param_bug.lean.expected.out
pp_struct.lean feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
pp_struct.lean.expected.out feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
pp_zero_bug.lean fix(frontends/lean/pp): bug when pretty printing partially applied polymorphic zero 2016-12-22 16:37:47 -08:00
pp_zero_bug.lean.expected.out fix(frontends/lean/pp): bug when pretty printing partially applied polymorphic zero 2016-12-22 16:37:47 -08:00
ppbug.lean
ppbug.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
print_ax1.lean
print_ax1.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
print_ax2.lean
print_ax2.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
print_ax3.lean feat(frontends/lean/print_cmd): show sorry macro as axiom 2017-02-05 14:01:08 +01:00
print_ax3.lean.expected.out feat(frontends/lean/print_cmd): show sorry macro as axiom 2017-02-05 14:01:08 +01:00
print_meta.lean chore(frontends/lean/print_cmd): update print command to keyword changes 2017-01-12 12:04:37 -08:00
print_meta.lean.expected.out chore(frontends/lean/print_cmd): update print command to keyword changes 2017-01-12 12:04:37 -08:00
print_reducible.lean
print_reducible.lean.expected.out
private_structure.lean fix(frontends/lean/structure_cmd): leftover 2016-09-10 12:57:24 -07:00
private_structure.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
prodtst.lean refactor(*): remove abbreviation command 2016-09-03 17:11:29 -07:00
prodtst.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
proj_notation.lean feat(frontends/lean): add aliases such as: .1 for ~>1 2016-09-21 11:32:02 -07:00
proj_notation.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
protected.lean
protected.lean.expected.out
protected_consts.lean
protected_consts.lean.expected.out
protected_test.lean chore(library/init/data/nat): rename nat.less_than to nat.less_than_or_equal as suggested by Rob 2017-01-11 17:47:49 -08:00
protected_test.lean.expected.out chore(library/init/data/nat): rename nat.less_than to nat.less_than_or_equal as suggested by Rob 2017-01-11 17:47:49 -08:00
qexpr1.lean
qexpr1.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
qexpr2.lean fix(library/init/meta,library/tactic/elaborate): bad error position when to_expr is used outside of interactive mode 2017-02-09 18:44:50 -08:00
qexpr2.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
qexpr3.lean
qexpr3.lean.expected.out
quot_abuse1.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
quot_abuse1.lean.expected.out chore(kernel/quotient/quotient): remove leftover 2017-01-26 13:05:09 -08:00
quot_abuse2.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
quot_abuse2.lean.expected.out chore(kernel/quotient/quotient): remove leftover 2017-01-26 13:05:09 -08:00
quot_bug.lean
quot_bug.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
quot_ind_bug.lean feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's 2017-01-24 15:59:38 -08:00
quot_ind_bug.lean.expected.out feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's 2017-01-24 15:59:38 -08:00
quote_error_pos.lean fix(frontends/lean/tactic_notation): erase position information quoted terms occurring inside `[...] 2017-02-09 19:06:56 -08:00
quote_error_pos.lean.expected.out fix(frontends/lean/tactic_notation): erase position information quoted terms occurring inside `[...] 2017-02-09 19:06:56 -08:00
readlinkf.sh fix(test_single.sh): OSX compatibility 2016-12-01 11:03:11 -08:00
record_rec_protected.lean
record_rec_protected.lean.expected.out
red.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
red.lean.expected.out feat(frontends/lean/elaborator): improve error messages for eliminators 2016-09-29 11:29:59 -07:00
refine_error.lean fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
refine_error.lean.expected.out fix(frontends/lean/elaborator, kernel/error_msgs): (re-)activate distinguishing_pp_options 2017-01-30 11:54:00 -08:00
reserve_bugs.lean
reserve_bugs.lean.expected.out
restrict_bug.lean
restrict_bug.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
rev_tac1.lean
rev_tac1.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
right_assoc_dollar.lean chore(library/init/function): make '$' right assoc like Haskell 2016-10-02 07:25:50 -07:00
right_assoc_dollar.lean.expected.out chore(library/init/function): make '$' right assoc like Haskell 2016-10-02 07:25:50 -07:00
rquote.lean
rquote.lean.expected.out
sec.lean
sec.lean.expected.out
sec3.lean
sec3.lean.expected.out
sec_param_pp.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
sec_param_pp.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
sec_param_pp2.lean
sec_param_pp2.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
set_attr1.lean chore(tests/lean): fix tests 2016-11-05 11:51:29 -07:00
set_attr1.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
set_of.lean feat(frontends/lean/pp): pretty print set_of notation 2016-09-24 13:55:02 -07:00
set_of.lean.expected.out feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
set_opt_tac.lean
set_opt_tac.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
shadow.lean chore(tests/lean): make sure all tests can be processed using new elaborator 2016-09-19 16:17:32 -07:00
shadow.lean.expected.out
showenv.l
slow_error.lean test(tests/lean/slow_error): add test that exposed perf problem in type context 2016-10-04 02:06:25 -07:00
slow_error.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
smt_begin_end1.lean feat(library/tactic/smt/smt_state): do not apply intros automatically in begin[smt]...end blocks 2017-01-12 21:49:17 -08:00
smt_begin_end1.lean.expected.out fix(frontends/lean/tactic_evaluator): 'begin [smt] ... end' block nested in regular one 2017-01-07 13:35:43 -08:00
struct_class.lean feat(library/init): add basic algebra 2016-09-30 20:51:22 -07:00
struct_class.lean.expected.out refactor(library/init/core): simpler has_sep type class with out_param 2017-01-30 18:54:56 -08:00
structure_instance_bug.lean fix(frontends/lean/elaborator): structure instance notation {...} for structures that have implicit fields 2016-09-23 11:32:12 -07:00
structure_instance_bug.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
structure_instance_bug2.lean refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
structure_instance_bug2.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
structure_result_type_may_be_zero.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
structure_result_type_may_be_zero.lean.expected.out feat(frontends/lean): use new notation for declaring universes in constant and structure decls 2016-09-13 21:45:16 -07:00
structure_with_index_error.lean
structure_with_index_error.lean.expected.out
subpp.lean feat(frontends/lean): change subtype notation (again) 2016-09-21 17:02:18 -07:00
subpp.lean.expected.out feat(frontends/lean): change subtype notation (again) 2016-09-21 17:02:18 -07:00
subst_bug.lean
subst_bug.lean.expected.out chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
synth_inferred_mismatch.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
synth_inferred_mismatch.lean.expected.out chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
t2.lean
t2.lean.expected.out
t5.lean feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
t5.lean.expected.out feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
t6.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
t6.lean.expected.out
t10.lean
t10.lean.expected.out chore(tests/lean): fix tests after error-recovery 2017-02-06 15:15:47 +01:00
t11.lean
t11.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
t12.lean
t12.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
t13.lean
t13.lean.expected.out chore(library/pp_options): pp.binder_types true by default 2016-09-14 09:02:42 -07:00
t14.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
t14.lean.expected.out
tactic_failure.lean
tactic_failure.lean.expected.out chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
tactic_state_pp.lean fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
tactic_state_pp.lean.expected.out chore(tests/lean): adjust tests to recent changes 2017-01-20 19:08:41 -08:00
task.lean feat(init/meta/async_tactic): add tactic to prove subgoals in a different task 2017-01-28 08:27:23 +01:00
task.lean.expected.out feat(init/meta/async_tactic): add tactic to prove subgoals in a different task 2017-01-28 08:27:23 +01:00
test.sh feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
test_single.sh feat(tests/lean/test_single): show unified diffs with color 2017-02-05 13:44:21 +01:00
test_single_pp.sh feat(*): parallel compilation 2016-11-29 11:12:40 -08:00
trace1.lean
trace1.lean.expected.out
trace2.lean
trace2.lean.expected.out
try_for_heap.lean feat(library/tactic): add try_for tactic 2017-02-11 20:35:42 -08:00
try_for_heap.lean.expected.out chore(tests/lean): fix tests 2017-02-12 16:50:42 -08:00
tuple.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
tuple.lean.expected.out chore(tests/lean): make sure all tests can be processed using new elaborator 2016-09-19 16:17:32 -07:00
type_class_bug.lean
type_class_bug.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
unfold1.lean refactor(library/init/meta): avoid '_core' idiom using default parameters 2017-02-14 09:46:55 -08:00
unfold1.lean.expected.out feat(library/init/meta): implement unfold tactics in Lean using new building blocks 2016-10-12 17:25:56 -07:00
unfold_crash.lean feat(library/init/meta): implement unfold tactics in Lean using new building blocks 2016-10-12 17:25:56 -07:00
unfold_crash.lean.expected.out feat(library/init/meta): implement unfold tactics in Lean using new building blocks 2016-10-12 17:25:56 -07:00
uni_bug1.lean refactor(library): rename pr1/pr2 ==> fst/snd 2016-09-21 09:48:39 -07:00
uni_bug1.lean.expected.out feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
unification_hints1.lean refactor(library/init): move unification_hint structure to init folder 2016-09-28 09:35:19 -07:00
unification_hints1.lean.expected.out refactor(*): structured message objects 2016-10-13 18:49:10 -07:00
unify3.lean
unify3.lean.expected.out
unify_tac1.lean
unify_tac1.lean.expected.out chore(tests): update tests to new position information for by tac 2016-11-30 11:27:02 -05:00
univ.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
univ.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
univ_vars.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
univ_vars.lean.expected.out feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
user_attribute.lean feat(frontends/lean): structure instances 2016-09-21 22:52:43 -07:00
user_attribute.lean.expected.out chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
utf8.lean
utf8.lean.expected.out
var.lean
var.lean.expected.out
var2.lean
var2.lean.expected.out feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
vm_eval_crash.lean
vm_eval_crash.lean.expected.out
vm_let_expr.lean feat(frontends/lean, library/init): add 'thunk' gadget 2017-01-31 18:41:59 -08:00
vm_let_expr.lean.expected.out test(tests/lean/vm_let_expr): add regression test for bugs fixed in the previous two commits 2017-01-12 11:18:16 -08:00
vm_sorry.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
vm_sorry.lean.expected.out fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
whnf.lean
whnf.lean.expected.out feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
whnf_cache_bug.lean
whnf_cache_bug.lean.expected.out feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
whnf_core1.lean refactor(library/init/meta): remove whnf_core 2017-02-14 18:39:57 -08:00
whnf_core1.lean.expected.out feat(frontends/lean/pp): pretty print structure instances and field projections 2017-02-05 14:01:53 -08:00
wrong_arity.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
wrong_arity.lean.expected.out fix(frontends/lean): 'sorry' axiom auto generation 2016-12-08 10:31:52 -08:00