Leonardo de Moura 9d3aa5b627 fix(library/compiler/elim_recursors): bug in elim_recursors ... We may fail to type check auxiliary definitions that use rec_fn_macro. The problem is that this macro cannot be unfolded. So, we fix the problem by not type checking them. We add them as constants, and store the definition in an auxiliary vector.		2016-11-02 14:19:28 -07:00
..
extra	chore(frontends/lean): new_elaborator is now the default	2016-09-19 16:34:06 -07:00
perf	chore(library, tests): switch to new attribute declaration syntax	2016-08-12 15:36:12 -07:00
run	fix(library/compiler/elim_recursors): bug in elim_recursors	2016-11-02 14:19:28 -07: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	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07: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	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
634.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
634b.lean	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
634b.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07: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(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
634d.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07: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	refactor(library/init/core): define nat.add using equations	2016-10-11 14:10:49 -07: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	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
1162.lean	feat(library/equations_compiler/elim_match): report unused equations	2016-10-19 09:58:08 -07:00
1162.lean.expected.out	feat(library/equations_compiler/elim_match): report unused equations	2016-10-19 09:58:08 -07: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(tests/lean): providing universes	2016-09-17 12:54:20 -07:00
anc1.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
assert_tac3.lean	chore(frontends/lean): coercions are disabled by default	2016-07-29 13:03:23 -07:00
assert_tac3.lean.expected.out	chore(library/pp_options): pp.binder_types true by default	2016-09-14 09:02:42 -07: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(library/tactic): add back notation for by assumption	2016-10-11 14:17:18 -07:00
attribute_bug1.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
attribute_bug1.lean.expected.out	refactor(library/tactic/simplify): delete old simplifier	2016-10-19 14:03:14 -07: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	feat(frontends/lean,library/tactic/tactic_state): improve error localization	2016-09-25 18:40:41 -07: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	feat(frontends/lean): add step-by-step 'begin...end' block execution	2016-09-26 10:56:40 -07:00
aux_decl_zeta.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
aux_decl_zeta.lean.expected.out	feat(frontends/lean/definition_cmds): improve error minimization	2016-09-23 10:16:46 -07:00
bad_end.lean
bad_end.lean.expected.out
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	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
bad_inaccessible2.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
bad_inaccessible2.lean.expected.out	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
bad_index.lean	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_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	fix(frontends/lean/structure_cmd): handle is_one_placeholder	2016-10-02 08:07:19 -07: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	feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command	2016-02-22 16:09:44 -08:00
bad_structures2.lean.expected.out	feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command	2016-02-22 16:09:44 -08:00
bug1.lean
bug1.lean.expected.out	feat(frontends/lean): lambda+anonymous_constructor+match notation	2016-09-21 08:49:05 -07: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(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07: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	feat(library/init/meta): rename rsimp* back to dsimp*	2016-10-11 16:37:08 -07:00
change1.lean.expected.out	feat(library/tactic): add 'change' tactic	2016-06-17 13:21:52 -07:00
change2.lean	feat(library/init/meta): rename rsimp* back to dsimp*	2016-10-11 16:37:08 -07:00
change2.lean.expected.out	feat(library/tactic/defeq_simplifier): invoke defeq_canonize from defeq_simp	2016-06-24 14:46:43 -07:00
char_lits.lean	feat(frontends/lean): add support for character literals	2016-07-18 14:07:10 -04:00
char_lits.lean.expected.out	refactor(*): structured message objects	2016-10-13 18:49:10 -07: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	feat(frontends/lean/elaborator): decorate error messages when overloads are used	2016-09-29 15:00:45 -07:00
cls_err.lean	chore(tests/lean): providing universes	2016-09-17 12:54:20 -07:00
cls_err.lean.expected.out	chore(tests/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07:00
coe1.lean	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
coe1.lean.expected.out	test(tests/lean/coe1): add coercion tests	2016-07-30 12:29:12 -07:00
coe2.lean	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
coe2.lean.expected.out	feat(frontends/lean/pp): add option for hiding coercions	2016-07-30 12:25:18 -07:00
coe3.lean	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
coe3.lean.expected.out	fix(library/type_context): bug in type class resolution	2016-07-30 15:54:28 -07:00
coe4.lean	feat(library/init/coe,frontends/lean): more general coercions to fun	2016-09-27 15:41:06 -07:00
coe4.lean.expected.out	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07: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/elaborator): coercions to sort	2016-07-30 19:47:04 -07:00
combinators1.lean	feat(library/init/meta/tactic): add 'focus', 'first', 'solve' and LCF-style AND_THEN tactical	2016-06-29 01:07:41 +01:00
combinators1.lean.expected.out	feat(library/tactic/intro_tactic): use get_unused_name	2016-09-19 16:38:03 -07:00
concrete_instance.lean	feat(library/init/algebra): make sure abstract instances do not override concrete ones	2016-10-01 13:48:46 -07:00
concrete_instance.lean.expected.out	refactor(*): structured message objects	2016-10-13 18:49:10 -07:00
config.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
config.lean.expected.out
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	chore(tests/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07:00
ctx.lean	chore(tests/lean): providing universes	2016-09-17 12:54:20 -07:00
ctx.lean.expected.out	chore(tests/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07: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	fix(tests/lean/ctx_error_msgs): avoid internal ids	2016-09-28 20:54:10 -07: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): change subtype notation (again)	2016-09-21 17:02:18 -07:00
curly_notation.lean.expected.out	feat(frontends/lean): change subtype notation (again)	2016-09-21 17:02:18 -07:00
def1.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
def1.lean.expected.out	feat(frontends/lean/elaborator): improve error messages for eliminators	2016-09-29 11:29:59 -07:00
def2.lean	feat(frontends/lean/definition_cmds): improve error minimization	2016-09-23 10:16:46 -07:00
def2.lean.expected.out	feat(frontends/lean/definition_cmds): improve error minimization	2016-09-23 10:16:46 -07: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(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
def_inaccessible_issue.lean	refactor(library/init/core): define nat.add using equations	2016-10-11 14:10:49 -07:00
def_inaccessible_issue.lean.expected.out	refactor(library/init/core): define nat.add using equations	2016-10-11 14:10:49 -07: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	feat(library/init/meta): rename rsimp* back to dsimp*	2016-10-11 16:37:08 -07:00
defeq1.lean.expected.out	feat(library/tactic): add tactic.defeq_simp	2016-06-17 11:20:15 -07:00
defeq_simp1.lean	feat(library/init/meta): rename rsimp* back to dsimp*	2016-10-11 16:37:08 -07:00
defeq_simp1.lean.expected.out	fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify	2016-10-12 08:33:40 -07: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	fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify	2016-10-12 08:33:40 -07: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	fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify	2016-10-12 08:33:40 -07: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	feat(src/library/defeq_canonizer): improve cache	2016-10-05 22:00:23 -07: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
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
elab1.lean	feat(frontends/lean): remove #elab command	2016-08-02 15:05:24 -07:00
elab1.lean.expected.out	feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result	2016-07-27 15:29:25 -07:00
elab2.lean	chore(tests/lean): providing universes	2016-09-17 12:54:20 -07:00
elab2.lean.expected.out	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07:00
elab3.lean	feat(frontends/lean): remove #elab command	2016-08-02 15:05:24 -07:00
elab3.lean.expected.out	feat(library/init/meta/tactic): universe polymorphic tactics	2016-10-25 03:42:55 +08:00
elab4.lean	chore(tests/lean): providing universes	2016-09-17 12:54:20 -07:00
elab4.lean.expected.out	feat(frontends/lean/elaborator): decorate error messages when overloads are used	2016-09-29 15:00:45 -07:00
elab4b.lean	chore(tests/lean): providing universes	2016-09-17 12:54:20 -07:00
elab4b.lean.expected.out	feat(frontends/lean/elaborator): decorate error messages when overloads are used	2016-09-29 15:00:45 -07:00
elab5.lean	feat(frontends/lean): remove #elab command	2016-08-02 15:05:24 -07:00
elab5.lean.expected.out	test(tests/lean): more examples	2016-07-27 16:08:33 -07:00
elab6.lean	chore(tests/lean): providing universes	2016-09-17 12:54:20 -07:00
elab6.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
elab7.lean	feat(frontends/lean): remove #elab command	2016-08-02 15:05:24 -07:00
elab7.lean.expected.out	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07: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	feat(frontends/lean/elaborator): decorate error messages when overloads are used	2016-09-29 15:00:45 -07:00
elab12.lean	feat(frontends/lean): remove #elab command	2016-08-02 15:05:24 -07:00
elab12.lean.expected.out	feat(frontends/lean/elaborator): display error when failed to elaborate using expected type	2016-09-29 11:55:05 -07: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	feat(frontends/lean/elaborator): improve error messages for eliminators	2016-09-29 11:29:59 -07:00
elab_error_msgs.lean.expected.out	refactor(*): structured message objects	2016-10-13 18:49:10 -07:00
elab_meta2.lean	feat(frontends/lean): 'mutual' and 'meta' are now keywords	2016-09-24 10:44:40 -07: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	chore(tests/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07: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	feat(library/type_context): solve ?m s =?= ?m t by first-order unification in approximate mode	2016-10-07 12:06:22 -07: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	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
eqn_hole.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
eqn_hole.lean.expected.out	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07: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	refactor(frontends/lean/elaborator): checkpoints	2016-09-14 17:29:51 -07: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): error localization bugs	2016-10-15 13:40:57 -07: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/type_context, library/tactic): add eta-expansion method and tactic	2016-08-14 16:15:12 -07:00
eta_tac.lean.expected.out	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07: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	feat(library/tactic/eval): eval_expr for arbitrary expressions	2016-10-03 19:01:22 -07:00
example_false.lean	fix(frontends/lean): type check examples	2016-09-27 14:39:55 -07:00
example_false.lean.expected.out	fix(frontends/lean): type check examples	2016-09-27 14:39:55 -07: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	feat(frontends/lean/definition_cmds): improve error minimization	2016-09-23 10:16:46 -07:00
focus_tac.lean	chore(frontends/lean): coercions are disabled by default	2016-07-29 13:03:23 -07:00
focus_tac.lean.expected.out	chore(tests/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07: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/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07:00
ftree.lean	chore(tests/lean): providing universes	2016-09-17 12:54:20 -07: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/scanner): hex scape in character literal	2016-07-19 12:38:20 -04:00
hex_char.lean.expected.out	feat(frontends/lean/scanner): hex scape in character literal	2016-07-19 12:38:20 -04:00
hex_numeral.lean	feat(frontends/lean/scanner): hexadecimal numerals	2016-07-19 13:04:27 -04:00
hex_numeral.lean.expected.out	feat(frontends/lean/scanner): hexadecimal numerals	2016-07-19 13:04:27 -04:00
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	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
hole_issue2.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
hole_issue2.lean.expected.out	feat(frontends/lean/elaborator): improve error messages for eliminators	2016-09-29 11:29:59 -07:00
inaccessible.lean	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
inaccessible.lean.expected.out	chore(tests/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07:00
inaccessible2.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
inaccessible2.lean.expected.out	feat(frontends/lean): lambda+anonymous_constructor+match notation	2016-09-21 08:49:05 -07:00
induction_tac1.lean	chore(frontends/lean): coercions are disabled by default	2016-07-29 13:03:23 -07: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
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/inst_error.lean.expected.out): fix output	2016-08-02 13:55:08 -07: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	feat(frontends/lean/definition_cmds): improve error minimization	2016-09-23 10:16:46 -07: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	fix(library/type_context): store instance fingerprint	2016-09-01 09:01:43 -07:00
internal_names.lean	fix(frontends/lean): uniform handling of declaration compound names	2016-06-02 18:13:50 -07:00
internal_names.lean.expected.out	fix(frontends/lean): uniform handling of declaration compound names	2016-06-02 18:13:50 -07:00
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(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
let1.lean.expected.out	feat(frontends/lean): lambda+anonymous_constructor+match notation	2016-09-21 08:49:05 -07: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
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	chore(tests/lean): fix tests	2016-06-16 18:47:23 -07: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
minimize_errors.lean	feat(frontends/lean): minimize errors being reported	2016-09-23 09:20:31 -07:00
minimize_errors.lean.expected.out	feat(frontends/lean/definition_cmds): improve error minimization	2016-09-23 10:16:46 -07:00
mismatch.lean
mismatch.lean.expected.out
namespace_bug.lean
namespace_bug.lean.expected.out	feat(frontends/lean): use new elaborator in the 'check' command	2016-08-02 14:57:49 -07:00
nary_overload.lean	feat(frontends/lean): use new notation for declaring universes in constant and structure decls	2016-09-13 21:45:16 -07:00
nary_overload.lean.expected.out	feat(frontends/lean/elaborator): decorate error messages when overloads are used	2016-09-29 15:00:45 -07:00
nat_pp.lean
nat_pp.lean.expected.out
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	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07: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	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
noncomp.lean
noncomp.lean.expected.out
noncomp_error.lean
noncomp_error.lean.expected.out
noncomp_thm.lean
noncomp_thm.lean.expected.out	chore(tests/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07: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	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
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	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
notation4.lean	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
notation4.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07: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
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	feat(frontends/lean): use new elaborator in the 'check' command	2016-08-02 14:57:49 -07:00
num2.lean.expected.out	feat(frontends/lean): use new elaborator in the 'check' command	2016-08-02 14:57:49 -07:00
num3.lean	chore(tests/lean): make sure tests only use init and systems.IO	2016-08-11 18:31:33 -07:00
num3.lean.expected.out	feat(frontends/lean): use new elaborator in the 'check' command	2016-08-02 14:57:49 -07:00
num4.lean	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
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
over_notation.lean	feat(frontends/lean): remove #elab command	2016-08-02 15:05:24 -07:00
over_notation.lean.expected.out	feat(frontends/lean/elaborator): decorate error messages when overloads are used	2016-09-29 15:00:45 -07: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(frontends/lean): remove dead code from parser	2016-09-19 17:04:59 -07: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
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	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07: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
pp_beta.lean.expected.out	chore(library/pp_options): pp.binder_types true by default	2016-09-14 09:02:42 -07:00
pp_binder_types.lean	feat(frontends/lean/pp): add option to hide binder types	2016-06-02 12:01:57 -07:00
pp_binder_types.lean.expected.out	chore(library/pp_options): pp.binder_types true by default	2016-09-14 09:02:42 -07:00
pp_bug.lean
pp_bug.lean.expected.out
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
ppbug.lean	chore(tests/lean): fix/disable tests	2016-06-10 18:29:41 -07:00
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	fix(tests/lean): tests	2016-09-23 16:29:41 -07:00
print_ax2.lean
print_ax2.lean.expected.out	fix(tests/lean): tests	2016-09-23 16:29:41 -07:00
print_ax3.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
print_ax3.lean.expected.out	fix(tests/lean): tests	2016-09-23 16:29:41 -07: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	feat(library/reducible): remove [quasireducible] annotation	2016-02-25 17:42:44 -08:00
private_structure.lean	fix(frontends/lean/structure_cmd): leftover	2016-09-10 12:57:24 -07:00
private_structure.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07: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	feat(frontends/lean/definition_cmds): improve error minimization	2016-09-23 10:16:46 -07: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
protected_test.lean.expected.out	chore(library/pp_options): pp.binder_types true by default	2016-09-14 09:02:42 -07:00
qexpr1.lean	feat(library/tactic, frontends/lean/elaborator): add to_expr tactic	2016-07-31 20:21:17 -07:00
qexpr1.lean.expected.out	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07:00
qexpr2.lean	fix(library/tactic/elaborate): new subgoals must be inserted after main goal	2016-07-31 21:16:29 -07:00
qexpr2.lean.expected.out	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07:00
qexpr3.lean	feat(library/init/meta/tactic): add 'refine' tactic	2016-07-31 21:17:19 -07:00
qexpr3.lean.expected.out	feat(library/init/meta/tactic): add 'refine' tactic	2016-07-31 21:17:19 -07:00
quot_bug.lean
quot_bug.lean.expected.out	chore(library/pp_options): pp.binder_types true by default	2016-09-14 09:02:42 -07:00
quot_ind_bug.lean	chore(library/init/quot): annotate quot eliminators	2016-09-10 22:51:07 -07:00
quot_ind_bug.lean.expected.out
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
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	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
rev_tac1.lean	chore(frontends/lean): coercions are disabled by default	2016-07-29 13:03:23 -07:00
rev_tac1.lean.expected.out	chore(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
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): adjust tests	2016-10-01 12:57:56 -07:00
set_attr1.lean.expected.out	fix(frontends/lean/elaborator): bad error msg	2016-09-29 15:23:20 -07: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 set_of notation	2016-09-24 13:55:02 -07:00
set_opt_tac.lean	chore(frontends/lean): coercions are disabled by default	2016-07-29 13:03:23 -07:00
set_opt_tac.lean.expected.out	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07: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	test(tests/lean/slow_error): add test that exposed perf problem in type context	2016-10-04 02:06:25 -07:00
struct_class.lean	feat(library/init): add basic algebra	2016-09-30 20:51:22 -07:00
struct_class.lean.expected.out	feat(library/init): add basic algebra	2016-09-30 20:51:22 -07: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/elaborator): structure instance notation {...} for structures that have implicit fields	2016-09-23 11:32:12 -07:00
structure_result_type_may_be_zero.lean	feat(frontends/lean): use new notation for declaring universes in constant and structure decls	2016-09-13 21:45:16 -07: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	fix(src/frontends/lean/structure_cmd): check if indices are provided	2016-06-14 17:52:19 -07:00
structure_with_index_error.lean.expected.out	fix(src/frontends/lean/structure_cmd): check if indices are provided	2016-06-14 17:52:19 -07:00
subpp.lean	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	fix(frontends/lean/elaborator): bad error msg	2016-09-29 15:23:20 -07: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
t3.lean	fix(frontends/lean): uniform handling of declaration compound names	2016-06-02 18:13:50 -07:00
t3.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
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	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07: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
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	feat(frontends/lean, library): remove attribute and metaclass scoping	2016-07-29 23:44:21 -04:00
t14.lean.expected.out	feat(frontends/lean, library): remove attribute and metaclass scoping	2016-07-29 23:44:21 -04:00
tactic_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/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07:00
test.sh
test_single.sh
test_single_pp.sh
trace1.lean	chore(frontends/lean): coercions are disabled by default	2016-07-29 13:03:23 -07:00
trace1.lean.expected.out	feat(library/init/meta/tactic): add 'when_tracing' tactical	2016-06-28 11:29:39 +01:00
trace2.lean	chore(frontends/lean): coercions are disabled by default	2016-07-29 13:03:23 -07:00
trace2.lean.expected.out	feat(frontends/lean): add declare_trace command	2016-06-28 11:45:56 +01:00
tuple.lean	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	feat(frontends/lean): anonymous instances	2016-09-23 13:34:34 -07:00
unfold1.lean	feat(library/init/meta): implement unfold tactics in Lean using new building blocks	2016-10-12 17:25:56 -07: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): add aliases such as: .1 for ~>1	2016-09-21 11:32:02 -07: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/lean): make sure all tests can be processed using new elaborator	2016-09-19 16:17:32 -07:00
univ.lean	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
univ.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
univ_vars.lean	chore(tests/lean): make sure tests only use init and systems.IO	2016-08-11 18:31:33 -07:00
univ_vars.lean.expected.out	feat(frontends/lean): Type is now (Type 1)	2016-09-17 14:30:54 -07:00
user_attribute.lean	feat(frontends/lean): structure instances	2016-09-21 22:52:43 -07:00
user_attribute.lean.expected.out	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
utf8.lean	feat(library/init/string): add utf8_length	2016-07-19 14:22:37 -04:00
utf8.lean.expected.out	feat(library/init/string): add utf8_length	2016-07-19 14:22:37 -04:00
var.lean	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
whnf.lean	feat(frontends/lean): use new elaborator in the 'check' command	2016-08-02 14:57:49 -07:00
whnf.lean.expected.out	refactor(library/init/core): define nat.add using equations	2016-10-11 14:10:49 -07: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	refactor(library/init/core): define nat.add using equations	2016-10-11 14:10:49 -07:00
whnf_core1.lean	feat(library/tactic/tactic_state): add whnf_core	2016-08-14 16:02:40 -07:00
whnf_core1.lean.expected.out	refactor(library/init/core): define nat.add using equations	2016-10-11 14:10:49 -07:00
wrong_arity.lean	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00
wrong_arity.lean.expected.out	chore(frontends/lean): remove 'new_elaborator' option	2016-09-20 08:32:37 -07:00