lean4-htt

History

Leonardo de Moura 89daecb568 fix(library/type_context): assertion violation fixes #1335		2017-01-25 16:05:23 -08:00
..
extra
fail	feat(frontends/lean/parser): keep list of tasks that have to succeed	2017-01-17 15:31:17 -08:00
interactive	feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's	2017-01-24 15:59:38 -08:00
native_run
perf
run	fix(library/type_context): assertion violation	2017-01-25 16:05:23 -08:00
server
slow
smt2
trust0
trust10
584a.lean
584a.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
584b.lean
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	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
712.lean
712.lean.expected.out
858.lean
858.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
1162.lean
1162.lean.expected.out
1207.lean
1207.lean.expected.out
1258.lean
1258.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
1277.lean	chore(tests/lean/1277): remove trace	2017-01-23 18:40:22 -08:00
1277.lean.expected.out	chore(tests/lean/1277): remove trace	2017-01-23 18:40:22 -08:00
1279.lean	fix(frontends/lean/elaborator): cactch app_exception when trying to create coercion	2017-01-03 09:03:00 -08:00
1279.lean.expected.out	fix(frontends/lean/elaborator): cactch app_exception when trying to create coercion	2017-01-03 09:03:00 -08:00
1290.lean	fix(frontends/lean/parser): fixes #1290	2017-01-09 15:35:25 -08:00
1290.lean.expected.out	fix(frontends/lean/parser): fixes #1290	2017-01-09 15:35:25 -08:00
1292.lean	fix(frontends/lean): fixes #1292	2017-01-09 15:53:37 -08:00
1292.lean.expected.out	fix(frontends/lean): fixes #1292	2017-01-09 15:53:37 -08:00
1293.lean	fix(library/tactic/tactic_state): closes #1293	2017-01-09 16:23:02 -08:00
1293.lean.expected.out	fix(library/tactic/tactic_state): closes #1293	2017-01-09 16:23:02 -08:00
1299.lean	fix(frontends/lean/definition_cmds): fix #1299	2017-01-10 14:38:46 -08:00
1299.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
1327.lean	fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching	2017-01-21 22:38:17 -08:00
1327.lean.expected.out	fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching	2017-01-21 22:38:17 -08:00
alias.lean
alias.lean.expected.out
alias2.lean
alias2.lean.expected.out
anc1.lean
anc1.lean.expected.out	chore(library/init/meta/tactic): make all arguments in id_locked explicit.	2016-12-26 18:22:37 -08:00
assert_tac3.lean
assert_tac3.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
assumption_tac_notation.lean
assumption_tac_notation.lean.expected.out
attribute_bug1.lean
attribute_bug1.lean.expected.out
attributes.lean
attributes.lean.expected.out
auto_quote_error.lean
auto_quote_error.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
auto_quote_error2.lean
auto_quote_error2.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
aux_decl_zeta.lean
aux_decl_zeta.lean.expected.out
bad_end.lean
bad_end.lean.expected.out	fix(frontends/lean): bad position at spurious 'end' token	2016-12-29 19:51:36 -08:00
bad_end_error_pos.lean	fix(frontends/lean): bad position at spurious 'end' token	2016-12-29 19:51:36 -08:00
bad_end_error_pos.lean.expected.out	fix(frontends/lean): bad position at spurious 'end' token	2016-12-29 19:51:36 -08:00
bad_error1.lean
bad_error1.lean.expected.out
bad_error2.lean
bad_error2.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
bad_error3.lean	feat(frontends/lean/elaborator): catch error early	2017-01-05 13:37:55 -08:00
bad_error3.lean.expected.out	feat(frontends/lean/elaborator): catch error early	2017-01-05 13:37:55 -08:00
bad_error4.lean	feat(frontends/lean/elaborator): catch exception at is_def_eq	2017-01-06 08:16:51 -08:00
bad_error4.lean.expected.out	feat(frontends/lean/elaborator): catch exception at is_def_eq	2017-01-06 08:16:51 -08:00
bad_error5.lean	fix(frontends/lean/tactic_evaluator): show VM errors on tactic	2017-01-10 14:42:48 -08:00
bad_error5.lean.expected.out	feat(library/vm/vm_aux): add vm code for sorry	2017-01-22 14:18:38 -08:00
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
bad_structures.lean.expected.out
bad_structures2.lean
bad_structures2.lean.expected.out
begin_end_bug.lean	fix(frontends/lean): begin...end block scope	2017-01-03 21:01:14 -08:00
begin_end_bug.lean.expected.out	fix(frontends/lean): begin...end block scope	2017-01-03 21:01:14 -08:00
bug1.lean
bug1.lean.expected.out
by_contradiction.lean
by_contradiction.lean.expected.out
caching_user_attribute.lean
caching_user_attribute.lean.expected.out
calc1.lean
calc1.lean.expected.out
change1.lean
change1.lean.expected.out
change2.lean
change2.lean.expected.out
char_lits.lean
char_lits.lean.expected.out
check.lean
check.lean.expected.out
check2.lean
check2.lean.expected.out
choice_expl.lean
choice_expl.lean.expected.out
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
coe4.lean.expected.out
coe5.lean
coe5.lean.expected.out
coe6.lean
coe6.lean.expected.out
combinators1.lean
combinators1.lean.expected.out
concrete_instance.lean
concrete_instance.lean.expected.out
config.lean.expected.out
const.lean
const.lean.expected.out
crash.lean
crash.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
ctx.lean
ctx.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
ctx_error_msgs.lean
ctx_error_msgs.lean.expected.out
ctxopt.lean
ctxopt.lean.expected.out
curly_notation.lean
curly_notation.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
def1.lean
def1.lean.expected.out
def2.lean
def2.lean.expected.out
def3.lean
def3.lean.expected.out
def4.lean
def4.lean.expected.out
def_inaccessible_issue.lean	feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names	2017-01-06 11:40:34 -08:00
def_inaccessible_issue.lean.expected.out	feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names	2017-01-06 11:40:34 -08:00
def_ite_value.lean
def_ite_value.lean.expected.out
defeq1.lean
defeq1.lean.expected.out
defeq_simp1.lean	fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching	2017-01-21 22:38:17 -08:00
defeq_simp1.lean.expected.out	chore(tests/lean): fix tests output	2017-01-06 20:30:11 -08:00
defeq_simp2.lean
defeq_simp2.lean.expected.out
defeq_simp3.lean
defeq_simp3.lean.expected.out	chore(tests/lean): fix tests output	2017-01-06 20:30:11 -08:00
defeq_simp4.lean
defeq_simp4.lean.expected.out	chore(tests/lean): fix tests output	2017-01-06 20:30:11 -08:00
defeq_simp5.lean
defeq_simp5.lean.expected.out
dep_bug.lean
dep_bug.lean.expected.out
dsimp_whnf.lean
dsimp_whnf.lean.expected.out
dsimp_whnf_post.lean
dsimp_whnf_post.lean.expected.out
dunfold_constant.lean
dunfold_constant.lean.expected.out
elab1.lean
elab1.lean.expected.out
elab2.lean
elab2.lean.expected.out
elab3.lean
elab3.lean.expected.out
elab4.lean
elab4.lean.expected.out
elab4b.lean
elab4b.lean.expected.out
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
elab12.lean
elab12.lean.expected.out
elab13.lean
elab13.lean.expected.out
elab14.lean
elab14.lean.expected.out
elab15.lean
elab15.lean.expected.out
elab_error_msgs.lean
elab_error_msgs.lean.expected.out
elab_meta2.lean
elab_meta2.lean.expected.out
empty.lean
empty.lean.expected.out
emptyc_errors.lean
emptyc_errors.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
eqn_compiler_loop.lean
eqn_compiler_loop.lean.expected.out
eqn_hole.lean
eqn_hole.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
error_full_names.lean
error_full_names.lean.expected.out
error_pos.lean
error_pos.lean.expected.out
errors2.lean
errors2.lean.expected.out
eta_bug.lean
eta_bug.lean.expected.out
eta_tac.lean	feat(library/init/meta/tactic): add eta reduction tactic	2017-01-06 19:56:10 -08:00
eta_tac.lean.expected.out	feat(library/init/meta/tactic): add eta reduction tactic	2017-01-06 19:56:10 -08:00
eval_expr_error.lean
eval_expr_error.lean.expected.out
example_false.lean
example_false.lean.expected.out
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
hinst_lemmas1.lean	feat(library/tactic/smt/hinst_lemmas): change how transparency is used to process hinst_lemmas	2017-01-04 19:12:37 -08:00
hinst_lemmas1.lean.expected.out	fix(library/tactic/smt/hinst_lemmas): pattern normalization issue	2017-01-08 23:35:39 -08:00
hinst_lemmas2.lean	feat(library/init/meta/smt/ematch): add commands for creating attributes for hinst_lemmas	2017-01-04 20:31:38 -08:00
hinst_lemmas2.lean.expected.out	feat(library/init/meta/smt/ematch): add commands for creating attributes for hinst_lemmas	2017-01-04 20:31:38 -08:00
hole_in_fn.lean
hole_in_fn.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
hole_issue2.lean	feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's	2017-01-24 15:59:38 -08:00
hole_issue2.lean.expected.out	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
import_invalid_tk.lean	feat(frontends/lean/parser): gracefully handle scanner exceptions in imports	2017-01-11 23:49:44 -08:00
import_invalid_tk.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
import_middle.lean	feat(frontends/lean/builtin_cmds): improve error message when import is used in the middle of the file	2017-01-11 11:15:29 -08:00
import_middle.lean.expected.out	feat(frontends/lean/builtin_cmds): improve error message when import is used in the middle of the file	2017-01-11 11:15:29 -08:00
inaccessible.lean
inaccessible.lean.expected.out
inaccessible2.lean
inaccessible2.lean.expected.out
induction_tac1.lean
induction_tac1.lean.expected.out
inductive_cmd_leftover_placeholder_universe.lean
inductive_cmd_leftover_placeholder_universe.lean.expected.out
inline_issue.lean	fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied	2017-01-17 16:33:19 -08:00
inline_issue.lean.expected.out	fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied	2017-01-17 16:33:19 -08:00
inst.lean
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
int_eval.lean
int_eval.lean.expected.out
internal_names.lean
internal_names.lean.expected.out
io_bug1.lean	fix(library/compiler/erase_irrelevant): make sure io monad actions are not erased by dead code elimination optimization	2017-01-02 01:42:36 -08:00
io_bug1.lean.expected.out	fix(library/compiler/erase_irrelevant): make sure io monad actions are not erased by dead code elimination optimization	2017-01-02 01:42:36 -08:00
key_eqv1.lean
key_eqv1.lean.expected.out
let1.lean
let1.lean.expected.out
let3.lean
let3.lean.expected.out
let4.lean
let4.lean.expected.out
let_elim_issue.lean
let_elim_issue.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
local_ref_bugs.lean
local_ref_bugs.lean.expected.out
match_bug.lean
match_bug.lean.expected.out
minimize_errors.lean
minimize_errors.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
mismatch.lean
mismatch.lean.expected.out
missing_import.lean
missing_import.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
namespace_bug.lean
namespace_bug.lean.expected.out
nary_overload.lean
nary_overload.lean.expected.out
nat_add_assoc_no_axioms.lean	feat(tests/lean): add test to make sure simplifier did not introduce unwanted propext	2017-01-20 20:28:49 -08:00
nat_add_assoc_no_axioms.lean.expected.out	feat(tests/lean): add test to make sure simplifier did not introduce unwanted propext	2017-01-20 20:28:49 -08:00
nat_pp.lean
nat_pp.lean.expected.out
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	refactor(frontends/lean): interactive tactic support	2017-01-21 22:38:47 -08:00
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
notation8.lean.expected.out
notation_error_pos.lean	fix(frontends/lean/parser): position info when error is inside notation	2017-01-16 10:29:00 -08:00
notation_error_pos.lean.expected.out	fix(frontends/lean/parser): position info when error is inside notation	2017-01-16 10:29:00 -08:00
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
open_namespaces.lean
open_namespaces.lean.expected.out
over_notation.lean
over_notation.lean.expected.out
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	chore(tests/lean): adjust tests to recent changes	2017-01-20 19:08:41 -08:00
pp_all2.lean
pp_all2.lean.expected.out
pp_beta.lean	chore(tests/lean): adjust tests to recent changes	2017-01-20 19:08:41 -08:00
pp_beta.lean.expected.out	chore(tests/lean): adjust tests to recent changes	2017-01-20 19:08:41 -08:00
pp_binder_types.lean
pp_binder_types.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
pp_bug.lean
pp_bug.lean.expected.out
pp_char_bug.lean	fix(library/string,library/init/data/to_string): handle ASCII control characters	2017-01-11 23:44:33 -08:00
pp_char_bug.lean.expected.out	fix(library/string,library/init/data/to_string): handle ASCII control characters	2017-01-11 23:44:33 -08:00
pp_goal_issue.lean
pp_goal_issue.lean.expected.out
pp_no_proofs.lean
pp_no_proofs.lean.expected.out
pp_param_bug.lean
pp_param_bug.lean.expected.out
pp_zero_bug.lean
pp_zero_bug.lean.expected.out
ppbug.lean
ppbug.lean.expected.out
print_ax1.lean
print_ax1.lean.expected.out	feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's	2017-01-24 15:59:38 -08:00
print_ax2.lean
print_ax2.lean.expected.out	feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's	2017-01-24 15:59:38 -08:00
print_ax3.lean
print_ax3.lean.expected.out	feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's	2017-01-24 15:59:38 -08:00
print_meta.lean	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
print_meta.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
print_reducible.lean
print_reducible.lean.expected.out
private_structure.lean
private_structure.lean.expected.out	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
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	chore(library/init/data/nat): rename nat.less_than to nat.less_than_or_equal as suggested by Rob	2017-01-11 17:47:49 -08:00
protected_test.lean.expected.out	chore(library/init/data/nat): rename nat.less_than to nat.less_than_or_equal as suggested by Rob	2017-01-11 17:47:49 -08:00
qexpr1.lean
qexpr1.lean.expected.out
qexpr2.lean
qexpr2.lean.expected.out
qexpr3.lean
qexpr3.lean.expected.out
quot_bug.lean
quot_bug.lean.expected.out
quot_ind_bug.lean	feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's	2017-01-24 15:59:38 -08:00
quot_ind_bug.lean.expected.out	feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's	2017-01-24 15:59:38 -08:00
readlinkf.sh
record_rec_protected.lean
record_rec_protected.lean.expected.out
red.lean
red.lean.expected.out
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
right_assoc_dollar.lean.expected.out
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
set_attr1.lean.expected.out
set_of.lean
set_of.lean.expected.out
set_opt_tac.lean
set_opt_tac.lean.expected.out
shadow.lean
shadow.lean.expected.out
showenv.l
slow_error.lean
slow_error.lean.expected.out
smt_begin_end1.lean	feat(library/tactic/smt/smt_state): do not apply intros automatically in `begin[smt]...end` blocks	2017-01-12 21:49:17 -08:00
smt_begin_end1.lean.expected.out	fix(frontends/lean/tactic_evaluator): 'begin [smt] ... end' block nested in regular one	2017-01-07 13:35:43 -08:00
struct_class.lean
struct_class.lean.expected.out
structure_instance_bug.lean
structure_instance_bug.lean.expected.out
structure_instance_bug2.lean	refactor(library/init/meta/smt): use default value for config structures	2017-01-23 14:18:06 -08:00
structure_instance_bug2.lean.expected.out	refactor(library/init/meta/smt): use default value for config structures	2017-01-23 14:18:06 -08:00
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
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
tactic_state_pp.lean	feat(library/tactic): allow user to write their own pretty printer for tactic states	2016-12-30 18:58:50 -08:00
tactic_state_pp.lean.expected.out	chore(tests/lean): adjust tests to recent changes	2017-01-20 19:08:41 -08:00
test.sh
test_single.sh
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
unfold1.lean.expected.out
unfold_crash.lean
unfold_crash.lean.expected.out
uni_bug1.lean
uni_bug1.lean.expected.out
unification_hints1.lean
unification_hints1.lean.expected.out
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	chore(frontends/lean/print_cmd): update print command to keyword changes	2017-01-12 12:04:37 -08:00
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
vm_let_expr.lean	test(tests/lean/vm_let_expr): add regression test for bugs fixed in the previous two commits	2017-01-12 11:18:16 -08:00
vm_let_expr.lean.expected.out	test(tests/lean/vm_let_expr): add regression test for bugs fixed in the previous two commits	2017-01-12 11:18:16 -08:00
vm_sorry.lean	feat(library/vm/vm_aux): add vm code for sorry	2017-01-22 14:18:38 -08:00
vm_sorry.lean.expected.out	feat(library/vm/vm_aux): add vm code for sorry	2017-01-22 14:18:38 -08:00
whnf.lean
whnf.lean.expected.out	chore(tests/lean): adjust tests to recent changes	2017-01-20 19:08:41 -08:00
whnf_cache_bug.lean
whnf_cache_bug.lean.expected.out	chore(tests/lean): adjust tests to recent changes	2017-01-20 19:08:41 -08:00
whnf_core1.lean
whnf_core1.lean.expected.out	chore(tests/lean): adjust tests to recent changes	2017-01-20 19:08:41 -08:00
wrong_arity.lean
wrong_arity.lean.expected.out