Leonardo de Moura d5aa92eaeb feat(library/tactic/tactic_state): add vm_obj introspection		2016-11-14 21:58:34 -08:00
..
extra	chore(frontends/lean): new_elaborator is now the default	2016-09-19 16:34:06 -07:00
interactive	fix(frontends/lean): fixes #1188	2016-11-10 15:08:25 -08:00
perf	chore(library, tests): switch to new attribute declaration syntax	2016-08-12 15:36:12 -07:00
run	feat(library/tactic/tactic_state): add vm_obj introspection	2016-11-14 21:58:34 -08: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	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	feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information	2016-11-09 16:51:48 -08:00
aux_decl_zeta.lean.expected.out	feat(library/compiler,frontends/lean/elaborator): (try to) preserve position information	2016-11-09 16:51:48 -08: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.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	fix(frontends/lean): fixes #1188	2016-11-10 15:08:25 -08: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): fixes #1188	2016-11-10 15:08:25 -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/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): fix tests	2016-11-05 11:51:29 -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	fix(tests/lean): remove config.lean	2016-11-13 09:38:40 -08:00
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