Leonardo de Moura d59410cc41 refactor(kernel): support only proof irrelevant mode		2016-09-27 17:18:52 -07:00
..
extra
perf
run	refactor(kernel): support only proof irrelevant mode	2016-09-27 17:18:52 -07:00
slow
smt2
trust0
trust10
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
712.lean
712.lean.expected.out
858.lean
858.lean.expected.out
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
attribute_bug1.lean
attribute_bug1.lean.expected.out
attributes.lean
attributes.lean.expected.out
auto_quote_error.lean
auto_quote_error.lean.expected.out
auto_quote_error2.lean
auto_quote_error2.lean.expected.out
aux_decl_zeta.lean
aux_decl_zeta.lean.expected.out
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
bad_structures.lean.expected.out
bad_structures2.lean
bad_structures2.lean.expected.out
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
config.lean
config.lean.expected.out
const.lean
const.lean.expected.out
crash.lean
crash.lean.expected.out
ctx.lean
ctx.lean.expected.out
ctxopt.lean
ctxopt.lean.expected.out
curly_notation.lean
curly_notation.lean.expected.out
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
def_inaccessible_issue.lean.expected.out
def_ite_value.lean
def_ite_value.lean.expected.out
defeq1.lean
defeq1.lean.expected.out
defeq_simp1.lean
defeq_simp1.lean.expected.out
defeq_simp2.lean
defeq_simp2.lean.expected.out
defeq_simp_lemmas1.lean
defeq_simp_lemmas1.lean.expected.out
defeq_simp_lemmas2.lean
defeq_simp_lemmas2.lean.expected.out
dep_bug.lean
dep_bug.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_meta2.lean
elab_meta2.lean.expected.out
empty.lean
empty.lean.expected.out
eqn_compiler_loop.lean
eqn_compiler_loop.lean.expected.out
eqn_hole.lean
eqn_hole.lean.expected.out
eqn_sanitizer1.lean
eqn_sanitizer1.lean.expected.out
error_full_names.lean
error_full_names.lean.expected.out
errors2.lean
errors2.lean.expected.out
eta_bug.lean
eta_bug.lean.expected.out
eta_tac.lean
eta_tac.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
hole_in_fn.lean
hole_in_fn.lean.expected.out
hole_issue2.lean
hole_issue2.lean.expected.out
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
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
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
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
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
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
print_ax2.lean
print_ax2.lean.expected.out
print_ax3.lean
print_ax3.lean.expected.out
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
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
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
simplifier_prove_failures.lean
simplifier_prove_failures.lean.expected.out
struct_class.lean
struct_class.lean.expected.out
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
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
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
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
whnf_cache_bug.lean
whnf_cache_bug.lean.expected.out
whnf_core1.lean
whnf_core1.lean.expected.out
wrong_arity.lean
wrong_arity.lean.expected.out