| .. |
|
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
|
chore(tests/lean): fix tests, and environment.decl_pos
|
2017-02-21 11:21:02 -08:00 |
|
native_run
|
feat(*): C++ code generator
|
2016-12-05 16:11:41 -08:00 |
|
perf
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
run
|
refactor(frontends/lean/{parser,util}): extract quote functions
|
2017-02-23 01:52:13 +01:00 |
|
server
|
fix(frontends/lean/parser): crash on Win 10
|
2016-11-07 21:30:19 -08:00 |
|
slow
|
chore(library): disable stdlib but init and systems folder
|
2016-08-11 18:42:10 -07:00 |
|
smt2
|
test(frontends/smt2): basic tests for parser and elaborator
|
2016-07-29 10:44:44 -07:00 |
|
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
|
feat(frontends/lean): quoted names
|
2016-07-22 19:06:57 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
assert_tac3.lean.expected.out
|
chore(frontends/lean/print_cmd): update print command to keyword changes
|
2017-01-12 12:04:37 -08:00 |
|
assertion1.lean
|
chore(tests/lean): fix test
|
2017-02-16 21:42:51 -08:00 |
|
assertion1.lean.expected.out
|
chore(tests/lean): fix test
|
2017-02-16 21:42:51 -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
|
feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters
|
2017-02-17 13:45:56 +01:00 |
|
bad_id.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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_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
|
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
|
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
|
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
|
feat(frontends/lean/elaborator): modify the pre-term for overloaded notation
|
2016-07-31 17:14:01 -07:00 |
|
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
|
feat(library/tactic/defeq_simplifier): invoke defeq_canonize from defeq_simp
|
2016-06-24 14:46:43 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
check.lean.expected.out
|
chore(library/pp_options): pp.binder_types true by default
|
2016-09-14 09:02:42 -07:00 |
|
check2.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
check2.lean.expected.out
|
fix(frontends/lean/builtin_cmds): non-determinism
|
2016-08-11 08:01:44 -07:00 |
|
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
|
fix(library/type_context): bug in type class resolution
|
2016-07-30 15:54:28 -07:00 |
|
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
|
feat(frontends/lean/elaborator): coercions to functions
|
2016-07-30 18:54:20 -07:00 |
|
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
|
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/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
|
fix(library/local_context): depends_on should take into account assigned metavariables
|
2016-08-25 13:49:54 -07:00 |
|
dep_bug.lean.expected.out
|
fix(library/local_context): depends_on should take into account assigned metavariables
|
2016-08-25 13:49:54 -07:00 |
|
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
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
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
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab3.lean.expected.out
|
feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters
|
2017-02-17 13:45:56 +01: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
|
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
|
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
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
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
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab11.lean.expected.out
|
chore(tests/lean): fix tests after error-recovery
|
2017-02-06 15:15:47 +01:00 |
|
elab12.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab12.lean.expected.out
|
chore(tests/lean): fix tests after error-recovery
|
2017-02-06 15:15:47 +01:00 |
|
elab13.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
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
|
feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters
|
2017-02-17 13:45:56 +01: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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
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
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
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
|
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
|
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
|
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 |
|
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
|
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 |
|
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
|
feat(library/init/meta): improve induction tactic interface
|
2017-02-17 10:58:51 -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
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
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
|
feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters
|
2017-02-17 13:45:56 +01: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
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
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
|
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
|
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
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
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
|
|
|
|
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
|
fix(frontends/lean/match_expr): nary match revision
|
2016-08-10 07:24:10 -07:00 |
|
meta_equation_pos.lean
|
fix(frontends/lean/definition_cmds): copy position for equation in meta definitions
|
2017-02-17 19:57:49 -08:00 |
|
meta_equation_pos.lean.expected.out
|
fix(frontends/lean/definition_cmds): copy position for equation in meta definitions
|
2017-02-17 19:57:49 -08:00 |
|
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
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
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
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
notation2.lean.expected.out
|
|
|
|
notation3.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
notation5.lean.expected.out
|
|
|
|
notation6.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
notation6.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
notation7.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
fix(library/init/function): '$' notation should be left-associative
|
2016-08-09 16:50:36 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
num.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
num4.lean.expected.out
|
|
|
|
num5.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
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
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
feat(library/tactic, frontends/lean/elaborator): add to_expr tactic
|
2016-07-31 20:21:17 -07:00 |
|
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
|
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_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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -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
|
chore(tests/lean): fix tests
|
2017-01-30 11:54:00 -08: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(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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
rquote.lean.expected.out
|
feat(frontends/lean): resolved quoted names
|
2016-08-05 17:04:36 -07:00 |
|
sec.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
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
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
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
|
feat(frontends/lean): new pattern matching validation
|
2016-08-07 11:31:11 -07:00 |
|
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
|
fix(library/tactic/subst_tactic): incorrect depends_on
|
2016-08-16 11:19:06 -07:00 |
|
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
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
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
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04: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
|
chore(tests): update tests to new position information for by tac
|
2016-11-30 11:27:02 -05:00 |
|
tactic_state_pp.lean
|
feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters
|
2017-02-17 13:45:56 +01: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
|
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 |
|
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
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
type_class_bug.lean.expected.out
|
chore(tests/lean): fix tests
|
2017-01-30 11:54:00 -08:00 |
|
unfold1.lean
|
feat(library/init/meta): improve induction tactic interface
|
2017-02-17 10:58:51 -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
|
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 |
|
unify_tac1.lean
|
feat(library/tactic/tactic_state): add is_def_eq and is_def_eq_core tactics
|
2016-08-16 11:08:03 -07:00 |
|
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
|
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
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
var.lean.expected.out
|
|
|
|
var2.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
var2.lean.expected.out
|
feat(frontends/lean): Type is now (Type 1)
|
2016-09-17 14:30:54 -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 |
|
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
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
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
|
fix(library/type_context): whnf cache bug
|
2016-08-18 18:04:19 -07:00 |
|
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 |
