| .. |
|
extra
|
|
|
|
interactive
|
fix(frontends/lean): fixes #1188
|
2016-11-10 15:08:25 -08:00 |
|
perf
|
|
|
|
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
|
|
|
|
smt2
|
|
|
|
trust0
|
feat(tests): run tests in emscripten build
|
2016-10-16 14:41:35 -07:00 |
|
trust10
|
feat(tests): run tests in emscripten build
|
2016-10-16 14:41:35 -07:00 |
|
584a.lean
|
|
|
|
584a.lean.expected.out
|
|
|
|
584b.lean
|
|
|
|
584b.lean.expected.out
|
|
|
|
584c.lean
|
|
|
|
584c.lean.expected.out
|
|
|
|
634.lean
|
|
|
|
634.lean.expected.out
|
|
|
|
634b.lean
|
|
|
|
634b.lean.expected.out
|
|
|
|
634c.lean
|
|
|
|
634c.lean.expected.out
|
|
|
|
634d.lean
|
|
|
|
634d.lean.expected.out
|
|
|
|
652.lean
|
|
|
|
652.lean.expected.out
|
|
|
|
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
|
|
|
|
858.lean
|
|
|
|
858.lean.expected.out
|
|
|
|
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
|
|
|
|
alias.lean.expected.out
|
|
|
|
alias2.lean
|
|
|
|
alias2.lean.expected.out
|
|
|
|
anc1.lean
|
|
|
|
anc1.lean.expected.out
|
|
|
|
assert_tac3.lean
|
|
|
|
assert_tac3.lean.expected.out
|
|
|
|
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
|
|
|
|
attribute_bug1.lean.expected.out
|
refactor(library/tactic/simplify): delete old simplifier
|
2016-10-19 14:03:14 -07:00 |
|
attributes.lean
|
|
|
|
attributes.lean.expected.out
|
|
|
|
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
|
|
|
|
bad_id.lean.expected.out
|
|
|
|
bad_inaccessible.lean
|
|
|
|
bad_inaccessible.lean.expected.out
|
|
|
|
bad_inaccessible2.lean
|
|
|
|
bad_inaccessible2.lean.expected.out
|
|
|
|
bad_index.lean
|
|
|
|
bad_index.lean.expected.out
|
|
|
|
bad_notation.lean
|
|
|
|
bad_notation.lean.expected.out
|
|
|
|
bad_open.lean
|
|
|
|
bad_open.lean.expected.out
|
|
|
|
bad_pattern2.lean
|
|
|
|
bad_pattern2.lean.expected.out
|
|
|
|
bad_print.lean
|
|
|
|
bad_print.lean.expected.out
|
|
|
|
bad_quoted_symbol.lean
|
|
|
|
bad_quoted_symbol.lean.expected.out
|
|
|
|
bad_set_option.lean
|
|
|
|
bad_set_option.lean.expected.out
|
|
|
|
bad_structures.lean
|
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
|
|
|
|
bad_structures2.lean.expected.out
|
|
|
|
bug1.lean
|
|
|
|
bug1.lean.expected.out
|
|
|
|
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
|
|
|
|
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
|
|
|
|
calc1.lean
|
feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword
|
2016-09-24 18:40:57 -07:00 |
|
calc1.lean.expected.out
|
|
|
|
change1.lean
|
feat(library/init/meta): rename rsimp* back to dsimp*
|
2016-10-11 16:37:08 -07:00 |
|
change1.lean.expected.out
|
|
|
|
change2.lean
|
feat(library/init/meta): rename rsimp* back to dsimp*
|
2016-10-11 16:37:08 -07:00 |
|
change2.lean.expected.out
|
|
|
|
char_lits.lean
|
|
|
|
char_lits.lean.expected.out
|
refactor(*): structured message objects
|
2016-10-13 18:49:10 -07:00 |
|
check.lean
|
|
|
|
check.lean.expected.out
|
|
|
|
check2.lean
|
|
|
|
check2.lean.expected.out
|
|
|
|
choice_expl.lean
|
|
|
|
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
|
|
|
|
cls_err.lean.expected.out
|
|
|
|
coe1.lean
|
|
|
|
coe1.lean.expected.out
|
|
|
|
coe2.lean
|
|
|
|
coe2.lean.expected.out
|
|
|
|
coe3.lean
|
|
|
|
coe3.lean.expected.out
|
|
|
|
coe4.lean
|
feat(library/init/coe,frontends/lean): more general coercions to fun
|
2016-09-27 15:41:06 -07:00 |
|
coe4.lean.expected.out
|
|
|
|
coe5.lean
|
feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class
|
2016-09-29 17:56:35 -07:00 |
|
coe5.lean.expected.out
|
|
|
|
coe6.lean
|
feat(library/init/coe,frontends/lean): more general coercions to fun
|
2016-09-27 15:41:06 -07:00 |
|
coe6.lean.expected.out
|
|
|
|
combinators1.lean
|
|
|
|
combinators1.lean.expected.out
|
|
|
|
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
|
|
|
|
const.lean.expected.out
|
|
|
|
crash.lean
|
|
|
|
crash.lean.expected.out
|
fix(frontends/lean): fixes #1188
|
2016-11-10 15:08:25 -08:00 |
|
ctx.lean
|
|
|
|
ctx.lean.expected.out
|
|
|
|
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
|
|
|
|
ctxopt.lean.expected.out
|
|
|
|
curly_notation.lean
|
|
|
|
curly_notation.lean.expected.out
|
|
|
|
def1.lean
|
|
|
|
def1.lean.expected.out
|
feat(frontends/lean/elaborator): improve error messages for eliminators
|
2016-09-29 11:29:59 -07:00 |
|
def2.lean
|
|
|
|
def2.lean.expected.out
|
|
|
|
def3.lean
|
|
|
|
def3.lean.expected.out
|
|
|
|
def4.lean
|
|
|
|
def4.lean.expected.out
|
|
|
|
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
|
|
|
|
def_ite_value.lean.expected.out
|
|
|
|
defeq1.lean
|
feat(library/init/meta): rename rsimp* back to dsimp*
|
2016-10-11 16:37:08 -07:00 |
|
defeq1.lean.expected.out
|
|
|
|
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
|
|
|
|
dep_bug.lean.expected.out
|
|
|
|
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
|
|
|
|
elab1.lean.expected.out
|
|
|
|
elab2.lean
|
|
|
|
elab2.lean.expected.out
|
|
|
|
elab3.lean
|
|
|
|
elab3.lean.expected.out
|
feat(library/init/meta/tactic): universe polymorphic tactics
|
2016-10-25 03:42:55 +08:00 |
|
elab4.lean
|
|
|
|
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
|
|
|
|
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
|
|
|
|
elab5.lean.expected.out
|
|
|
|
elab6.lean
|
|
|
|
elab6.lean.expected.out
|
|
|
|
elab7.lean
|
|
|
|
elab7.lean.expected.out
|
|
|
|
elab8.lean
|
|
|
|
elab8.lean.expected.out
|
|
|
|
elab9.lean
|
|
|
|
elab9.lean.expected.out
|
|
|
|
elab11.lean
|
|
|
|
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
|
|
|
|
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
|
|
|
|
elab13.lean.expected.out
|
|
|
|
elab14.lean
|
|
|
|
elab14.lean.expected.out
|
|
|
|
elab15.lean
|
|
|
|
elab15.lean.expected.out
|
|
|
|
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
|
|
|
|
empty.lean.expected.out
|
|
|
|
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
|
|
|
|
eqn_compiler_loop.lean.expected.out
|
|
|
|
eqn_hole.lean
|
|
|
|
eqn_hole.lean.expected.out
|
|
|
|
error_full_names.lean
|
|
|
|
error_full_names.lean.expected.out
|
|
|
|
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
|
|
|
|
eta_bug.lean.expected.out
|
|
|
|
eta_tac.lean
|
|
|
|
eta_tac.lean.expected.out
|
|
|
|
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
|
|
|
|
field_access.lean.expected.out
|
|
|
|
focus_tac.lean
|
|
|
|
focus_tac.lean.expected.out
|
|
|
|
fold.lean
|
|
|
|
fold.lean.expected.out
|
|
|
|
format_thunk1.lean
|
|
|
|
format_thunk1.lean.expected.out
|
|
|
|
ftree.lean
|
|
|
|
ftree.lean.expected.out
|
|
|
|
generalize1.lean
|
|
|
|
generalize1.lean.expected.out
|
|
|
|
hex_char.lean
|
|
|
|
hex_char.lean.expected.out
|
|
|
|
hex_numeral.lean
|
|
|
|
hex_numeral.lean.expected.out
|
|
|
|
hole_in_fn.lean
|
|
|
|
hole_in_fn.lean.expected.out
|
|
|
|
hole_issue2.lean
|
|
|
|
hole_issue2.lean.expected.out
|
feat(frontends/lean/elaborator): improve error messages for eliminators
|
2016-09-29 11:29:59 -07:00 |
|
inaccessible.lean
|
|
|
|
inaccessible.lean.expected.out
|
|
|
|
inaccessible2.lean
|
|
|
|
inaccessible2.lean.expected.out
|
|
|
|
induction_tac1.lean
|
|
|
|
induction_tac1.lean.expected.out
|
chore(tests/lean/induction_tac1): adjust output
|
2016-10-05 22:01:16 -07:00 |
|
inductive_cmd_leftover_placeholder_universe.lean
|
|
|
|
inductive_cmd_leftover_placeholder_universe.lean.expected.out
|
|
|
|
inst.lean
|
|
|
|
inst.lean.expected.out
|
|
|
|
inst_error.lean
|
|
|
|
inst_error.lean.expected.out
|
|
|
|
instance_cache1.lean
|
|
|
|
instance_cache1.lean.expected.out
|
|
|
|
instance_cache_bug1.lean
|
|
|
|
instance_cache_bug1.lean.expected.out
|
|
|
|
internal_names.lean
|
|
|
|
internal_names.lean.expected.out
|
|
|
|
key_eqv1.lean
|
|
|
|
key_eqv1.lean.expected.out
|
fix(tests): update to name hashing changes
|
2016-10-16 14:41:35 -07:00 |
|
let1.lean
|
|
|
|
let1.lean.expected.out
|
|
|
|
let3.lean
|
|
|
|
let3.lean.expected.out
|
|
|
|
let4.lean
|
|
|
|
let4.lean.expected.out
|
|
|
|
lift_coe_off.lean
|
|
|
|
lift_coe_off.lean.expected.out
|
|
|
|
list_monad1.lean
|
|
|
|
list_monad1.lean.expected.out
|
|
|
|
local_notation_bug2.lean
|
|
|
|
local_notation_bug2.lean.expected.out
|
|
|
|
match_bug.lean
|
|
|
|
match_bug.lean.expected.out
|
|
|
|
minimize_errors.lean
|
|
|
|
minimize_errors.lean.expected.out
|
|
|
|
mismatch.lean
|
|
|
|
mismatch.lean.expected.out
|
|
|
|
namespace_bug.lean
|
|
|
|
namespace_bug.lean.expected.out
|
|
|
|
nary_overload.lean
|
|
|
|
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
|
|
|
|
no_confusion_type.lean.expected.out
|
|
|
|
non_exhaustive_error.lean
|
|
|
|
non_exhaustive_error.lean.expected.out
|
|
|
|
noncomp.lean
|
|
|
|
noncomp.lean.expected.out
|
|
|
|
noncomp_error.lean
|
|
|
|
noncomp_error.lean.expected.out
|
|
|
|
noncomp_thm.lean
|
|
|
|
noncomp_thm.lean.expected.out
|
|
|
|
notation.lean
|
|
|
|
notation.lean.expected.out
|
|
|
|
notation2.lean
|
|
|
|
notation2.lean.expected.out
|
|
|
|
notation3.lean
|
|
|
|
notation3.lean.expected.out
|
|
|
|
notation4.lean
|
|
|
|
notation4.lean.expected.out
|
|
|
|
notation5.lean
|
|
|
|
notation5.lean.expected.out
|
|
|
|
notation6.lean
|
|
|
|
notation6.lean.expected.out
|
|
|
|
notation7.lean
|
|
|
|
notation7.lean.expected.out
|
|
|
|
notation8.lean
|
chore(library/init/function): make '$' right assoc like Haskell
|
2016-10-02 07:25:50 -07:00 |
|
notation8.lean.expected.out
|
|
|
|
num.lean
|
|
|
|
num.lean.expected.out
|
|
|
|
num2.lean
|
|
|
|
num2.lean.expected.out
|
|
|
|
num3.lean
|
|
|
|
num3.lean.expected.out
|
|
|
|
num4.lean
|
|
|
|
num4.lean.expected.out
|
|
|
|
num5.lean
|
|
|
|
num5.lean.expected.out
|
|
|
|
omit.lean
|
|
|
|
omit.lean.expected.out
|
|
|
|
over_notation.lean
|
|
|
|
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
|
|
|
|
param.lean.expected.out
|
|
|
|
param_binder_update.lean
|
|
|
|
param_binder_update.lean.expected.out
|
|
|
|
param_binder_update2.lean
|
|
|
|
param_binder_update2.lean.expected.out
|
|
|
|
parsing_only.lean
|
|
|
|
parsing_only.lean.expected.out
|
|
|
|
pp.lean
|
|
|
|
pp.lean.expected.out
|
|
|
|
pp_all.lean
|
|
|
|
pp_all.lean.expected.out
|
|
|
|
pp_all2.lean
|
|
|
|
pp_all2.lean.expected.out
|
|
|
|
pp_beta.lean
|
|
|
|
pp_beta.lean.expected.out
|
|
|
|
pp_binder_types.lean
|
|
|
|
pp_binder_types.lean.expected.out
|
|
|
|
pp_bug.lean
|
|
|
|
pp_bug.lean.expected.out
|
|
|
|
pp_no_proofs.lean
|
|
|
|
pp_no_proofs.lean.expected.out
|
|
|
|
pp_param_bug.lean
|
|
|
|
pp_param_bug.lean.expected.out
|
|
|
|
ppbug.lean
|
|
|
|
ppbug.lean.expected.out
|
|
|
|
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
|
|
|
|
print_ax3.lean.expected.out
|
fix(tests/lean): tests
|
2016-09-23 16:29:41 -07:00 |
|
print_reducible.lean
|
|
|
|
print_reducible.lean.expected.out
|
|
|
|
private_structure.lean
|
|
|
|
private_structure.lean.expected.out
|
|
|
|
prodtst.lean
|
|
|
|
prodtst.lean.expected.out
|
|
|
|
proj_notation.lean
|
|
|
|
proj_notation.lean.expected.out
|
|
|
|
protected.lean
|
|
|
|
protected.lean.expected.out
|
|
|
|
protected_consts.lean
|
|
|
|
protected_consts.lean.expected.out
|
|
|
|
protected_test.lean
|
|
|
|
protected_test.lean.expected.out
|
|
|
|
qexpr1.lean
|
|
|
|
qexpr1.lean.expected.out
|
|
|
|
qexpr2.lean
|
|
|
|
qexpr2.lean.expected.out
|
|
|
|
qexpr3.lean
|
|
|
|
qexpr3.lean.expected.out
|
|
|
|
quot_bug.lean
|
|
|
|
quot_bug.lean.expected.out
|
|
|
|
quot_ind_bug.lean
|
|
|
|
quot_ind_bug.lean.expected.out
|
|
|
|
record_rec_protected.lean
|
|
|
|
record_rec_protected.lean.expected.out
|
|
|
|
red.lean
|
feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword
|
2016-09-24 18:40:57 -07:00 |
|
red.lean.expected.out
|
feat(frontends/lean/elaborator): improve error messages for eliminators
|
2016-09-29 11:29:59 -07:00 |
|
reserve_bugs.lean
|
|
|
|
reserve_bugs.lean.expected.out
|
|
|
|
restrict_bug.lean
|
|
|
|
restrict_bug.lean.expected.out
|
|
|
|
rev_tac1.lean
|
|
|
|
rev_tac1.lean.expected.out
|
|
|
|
right_assoc_dollar.lean
|
chore(library/init/function): make '$' right assoc like Haskell
|
2016-10-02 07:25:50 -07:00 |
|
right_assoc_dollar.lean.expected.out
|
chore(library/init/function): make '$' right assoc like Haskell
|
2016-10-02 07:25:50 -07:00 |
|
rquote.lean
|
|
|
|
rquote.lean.expected.out
|
|
|
|
sec.lean
|
|
|
|
sec.lean.expected.out
|
|
|
|
sec3.lean
|
|
|
|
sec3.lean.expected.out
|
|
|
|
sec_param_pp.lean
|
|
|
|
sec_param_pp.lean.expected.out
|
|
|
|
sec_param_pp2.lean
|
|
|
|
sec_param_pp2.lean.expected.out
|
|
|
|
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
|
|
|
|
set_opt_tac.lean.expected.out
|
|
|
|
shadow.lean
|
|
|
|
shadow.lean.expected.out
|
|
|
|
showenv.l
|
|
|
|
slow_error.lean
|
test(tests/lean/slow_error): add test that exposed perf problem in type context
|
2016-10-04 02:06:25 -07:00 |
|
slow_error.lean.expected.out
|
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
|
|
|
|
structure_instance_bug.lean.expected.out
|
|
|
|
structure_result_type_may_be_zero.lean
|
|
|
|
structure_result_type_may_be_zero.lean.expected.out
|
|
|
|
structure_with_index_error.lean
|
|
|
|
structure_with_index_error.lean.expected.out
|
|
|
|
subpp.lean
|
|
|
|
subpp.lean.expected.out
|
|
|
|
subst_bug.lean
|
|
|
|
subst_bug.lean.expected.out
|
fix(frontends/lean/elaborator): bad error msg
|
2016-09-29 15:23:20 -07:00 |
|
synth_inferred_mismatch.lean
|
|
|
|
synth_inferred_mismatch.lean.expected.out
|
|
|
|
t2.lean
|
|
|
|
t2.lean.expected.out
|
|
|
|
t3.lean
|
|
|
|
t3.lean.expected.out
|
|
|
|
t5.lean
|
|
|
|
t5.lean.expected.out
|
|
|
|
t6.lean
|
|
|
|
t6.lean.expected.out
|
|
|
|
t10.lean
|
|
|
|
t10.lean.expected.out
|
|
|
|
t11.lean
|
|
|
|
t11.lean.expected.out
|
|
|
|
t12.lean
|
|
|
|
t12.lean.expected.out
|
|
|
|
t13.lean
|
|
|
|
t13.lean.expected.out
|
|
|
|
t14.lean
|
|
|
|
t14.lean.expected.out
|
|
|
|
tactic_failure.lean
|
|
|
|
tactic_failure.lean.expected.out
|
|
|
|
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
|
|
|
|
trace1.lean.expected.out
|
|
|
|
trace2.lean
|
|
|
|
trace2.lean.expected.out
|
|
|
|
tuple.lean
|
|
|
|
tuple.lean.expected.out
|
|
|
|
type_class_bug.lean
|
|
|
|
type_class_bug.lean.expected.out
|
|
|
|
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
|
|
|
|
uni_bug1.lean.expected.out
|
|
|
|
unification_hints1.lean
|
refactor(library/init): move unification_hint structure to init folder
|
2016-09-28 09:35:19 -07:00 |
|
unification_hints1.lean.expected.out
|
refactor(*): structured message objects
|
2016-10-13 18:49:10 -07:00 |
|
unify3.lean
|
|
|
|
unify3.lean.expected.out
|
|
|
|
unify_tac1.lean
|
|
|
|
unify_tac1.lean.expected.out
|
|
|
|
univ.lean
|
|
|
|
univ.lean.expected.out
|
|
|
|
univ_vars.lean
|
|
|
|
univ_vars.lean.expected.out
|
|
|
|
user_attribute.lean
|
|
|
|
user_attribute.lean.expected.out
|
|
|
|
utf8.lean
|
|
|
|
utf8.lean.expected.out
|
|
|
|
var.lean
|
|
|
|
var.lean.expected.out
|
|
|
|
var2.lean
|
|
|
|
var2.lean.expected.out
|
|
|
|
vm_eval_crash.lean
|
|
|
|
vm_eval_crash.lean.expected.out
|
|
|
|
whnf.lean
|
|
|
|
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
|
|
|
|
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
|
|
|
|
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
|
|
|
|
wrong_arity.lean.expected.out
|
|
|
