max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/run
History
Leonardo de Moura 19ee270c60 refactor(library): remove vector and bitvec from init 
Reason: vector in in init folder was introducing an overload (`::`) for
all Lean users. The workaround (use `local infix ::`) was
counterintuitive.

We currently have no special support for bitvectors in the code
generator. Thus, there is no need to have vector and bitvec in the init
folder right now. Moreover, the new parser and elaborator (issue #1674) should
provide better ways of managing overloaded symbols.
2017-08-16 13:40:50 -07:00
..
252.lean chore(tests/lean/run/252): fix test 2017-05-30 13:11:59 -07:00
331.lean
444.lean
445.lean
490.lean
600a.lean
600b.lean
600c.lean
662.lean
751.lean
774.lean
791.lean
808.lean
817.lean
967.lean
968.lean
1089.lean refactor(*): wrap string in a structure 2017-06-07 17:30:49 -07:00
1093.lean chore(library/init/meta): add to_unfold parameter to simplify, and remove redundant simp* tactics 2017-07-02 15:26:06 -07:00
1163.lean
1171.lean
1208.lean
1216.lean
1218.lean
1226.lean
1253.lean
1258.lean
1260.lean
1295.lean
1302.lean
1315a.lean
1315b.lean
1318.lean
1331.lean
1335.lean chore(library/standard): remove standard.lean (unused, and confusing given stdlib) 2017-07-28 16:47:53 +01:00
1343.lean
1414.lean
1430.lean
1433.lean
1442.lean
1458.lean
1493.lean
1495.lean feat(frontends/lean/tactic_notation): allow show keyword to be used as syntax sugar for the show_goal tactic 2017-06-01 18:52:54 -07:00
1525.lean
1557.lean
1562.lean
1577.lean
1585.lean fix(frontends/lean/structure_cmd): parent structures may use different universe params 2017-05-18 09:35:14 -07:00
1587.lean fix(library/tactic/rewrite_tactic): instantiate assign metavars before rewriting 2017-05-18 10:57:03 -07:00
1590.lean fix(init/meta/expr): have all reflected defns accept Sort 2017-05-23 11:00:33 +02:00
1594_comment_issue.lean fix(library/equations_compiler/elim_match): forward dependency checking 2017-06-20 11:29:23 -07:00
1608.lean feat(library/tactic/smt/congruence_closure): add builtin support for (@ne A a b) 2017-05-26 17:06:22 -07:00
1609.lean fix(library/constructions/injective): fixes #1609 2017-05-26 16:39:38 -07:00
1623.lean fix(frontends/lean/structure_cmd): use collect_implicit_locals to catch more context locals 2017-06-01 07:38:30 -07:00
1631.lean fix(library/noncomputable): fixes #1631 2017-05-31 23:16:37 -07:00
1649a.lean fix(frontends/lean): fixes #1649 2017-06-06 21:33:24 -07:00
1649b.lean fix(frontends/lean): fixes #1649 2017-06-06 21:33:24 -07:00
1650.lean fix(kernel/type_checker,library/type_context): add support for macros that cannot be expanded 2017-06-07 08:25:21 -07:00
1655.lean feat(frontends/lean/inductive_cmds): closes #1655 2017-06-20 16:25:18 -07:00
1657.lean fix(inductive_compiler/nested.cpp): fixes #1657 2017-06-09 20:06:50 +02:00
1658.lean fix(library/compiler/preprocess): compile_lemma => compile_irrelevant 2017-06-12 20:33:31 -07:00
1663.lean fix(library/equations_compiler): fixes #1663 2017-06-12 19:45:01 -07:00
1675.lean feat(library/init/meta/interactive): simp_all ==> simp * at * 2017-07-04 11:57:16 -07:00
1681.lean fix(frontends/lean/structure_cmd): fixes #1681 2017-06-19 16:22:38 -07:00
1682.lean fix(frontends/lean/elaborator): fixes #1682 2017-06-19 16:04:24 -07:00
1685.lean fix(library/tactic/simplify): fixes #1685 2017-06-20 12:27:46 -07:00
1686.lean fix(library/tactic/change_tactic): fixes #1686 2017-06-20 12:05:21 -07:00
1688.lean test(tests/lean/run/1688): add test for PR #1688 2017-06-20 12:36:31 -07:00
1703.lean fix(frontends/lean/brackets): fixes #1703 2017-06-26 12:52:52 -07:00
1705.lean refactor(*): move out stdlib 2017-07-26 11:52:10 +01:00
1718.lean refactor(frontends/lean/token_table,library): take ~> assume 2017-07-05 11:20:10 -07:00
1724.lean fix(library/init/meta/simp_tactic): fixes #1724 2017-07-05 11:59:23 -07:00
1728.lean fix(library/delayed_abstraction): fixes #1728 2017-07-05 17:10:18 -07:00
1733.lean fix(library/init/meta/interactive): fixes #1733 2017-07-06 22:34:24 -07:00
1739.lean fix(library/equations_compiler/elim_match): undo bcf44f7 2017-07-07 09:16:07 -07:00
1771.lean fix(library/init/meta/constructor_tactic): fixes #1771 2017-07-28 09:45:51 +01:00
1782.lean feat(library/equations_compiler/wf_rec): fixes #1782 2017-08-02 15:12:04 +01:00
abstract_ns.lean
abstract_ns1.lean
abstract_ns2.lean
abstract_tac.lean
abstract_zeta.lean
ac_refl1.lean
ack.lean feat(library/init/meta/well_founded_tactics): add simple tactic for discharging decreasing proofs 2017-05-23 22:07:46 -07:00
add_interactive.lean feat(library/init/meta/interactive): add add_interactive command. 2017-06-05 16:43:15 -07:00
add_semi.lean
aexp.lean feat(library/tactic/induction_tactic): clear hypothesis before introducing new ones 2017-07-07 10:06:30 -07:00
alg_info1.lean
algebra_attr.lean
all_goals1.lean
and_rec_code_gen_issue.lean feat(library/init/meta/interactive): simp and unfold can unfold projection applications 2017-07-02 16:28:04 -07:00
anonymous_param.lean
any_goals.lean
app_builder_tac1.lean
apply1.lean
apply2.lean
apply3.lean
apply4.lean feat(library/tactic/apply_tactic): make apply tactic more robust 2017-06-27 10:42:26 -07:00
apply_auto_opt.lean feat(library/init/meta): handle auto_params and opt_params at apply tactic 2017-06-27 18:17:48 -07:00
arity1.lean
array1.lean
array2.lean
as.lean
as_is_elab.lean
assert_tac1.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
assert_tac3.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
assoc_flat.lean
at_at_bug.lean
atomic2.lean
atomic_notation.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
auto_eq_congr_extra_args.lean
auto_param.lean
auto_param2.lean
auto_param_in_structures.lean chore(library/init/meta): add to_unfold parameter to simplify, and remove redundant simp* tactics 2017-07-02 15:26:06 -07:00
auto_propext.lean
auto_quote1.lean feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 2017-07-05 11:42:55 -07:00
auto_quote2.lean
back_chaining1.lean
back_chaining2.lean
back_chaining3.lean
back_chaining4.lean
basic.lean
basic_monitor.lean fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean 2017-06-18 18:33:27 -07:00
basic_monitor1.lean chore(tests): fix tests 2017-06-18 18:33:38 -07:00
basic_monitor2.lean
basic_monitor3.lean
begin_end1.lean
begin_end_do.lean
beta_zeta.lean
bin_oct_hex.lean
bin_tree.lean chore(tests/lean/run/bin_tree): fix broken test 2017-07-21 05:05:42 -07:00
blast_unit.lean
blast_unit2.lean
booltst.lean
bor_lazy.lean
bug5.lean
bug6.lean
bug_proving_eqn_lemmas.lean
calc.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
calc_auto_trans_eq.lean
calc_bug.lean
calc_heq_symm.lean
calc_imp.lean
calc_tac.lean
cases_bug.lean
cases_bug2.lean
cases_bug3.lean
cases_crash1.lean
cases_nested.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
cases_renaming_issue.lean
cases_tac1.lean feat(library/init/meta/simp_tactic): add option for reducing [reducible] definitions at dsimp, and to_unfold : list name similar to the one in the simp tactic 2017-07-03 13:28:46 -07:00
cases_term.lean
cast_sorry_bug.lean
cc1.lean
cc2.lean
cc3.lean
cc4.lean refactor(library): remove vector and bitvec from init 2017-08-16 13:40:50 -07:00
cc5.lean
cc6.lean
cc7.lean
cc_ac1.lean
cc_ac2.lean
cc_ac3.lean
cc_ac4.lean refactor(*): move out stdlib 2017-07-26 11:52:10 +01:00
cc_ac5.lean
cc_ac_bug.lean
cc_beta.lean
cc_constructors.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
cc_proj.lean
cc_value.lean
cheap_try_refl.lean
check_constants.lean refactor(library/init/algebra): remove order_pair classes 2017-08-02 14:41:35 +01:00
check_monad_mk.lean
check_tac.lean feat(library/init/meta): add type_check tactic 2017-06-25 15:26:32 -07:00
choice_anon_ctor.lean refactor(library): remove vector and bitvec from init 2017-08-16 13:40:50 -07:00
choice_ctx.lean
class1.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
class2.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
class3.lean
class6.lean
class11.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
cody2.lean
coe_opt.lean
coe_univ_bug.lean
coinductive.lean refactor(*): move out stdlib 2017-07-26 11:52:10 +01:00
comment.lean
comp_val1.lean
comp_val2.lean
comp_val3.lean
comp_val4.lean
compiler_bug1.lean
compiler_bug2.lean
compiler_bug3.lean
complete_rec_var.lean
confuse_ind.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
congr_lemma1.lean
congr_tactic.lean feat(init/meta/congr_tactic.lean): tactic to apply congruence rules 2017-06-26 09:17:53 -04:00
const_choice.lean
constructor1.lean
consume.lean
contra1.lean
contra2.lean
contra3.lean
contradiction_issue.lean
conv_tac1.lean feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 2017-07-05 11:42:55 -07:00
cpdt.lean feat(library/init/meta/interactive): simph ==> simp [*] 2017-07-03 15:14:47 -07:00
cute_binders.lean
dec_trivial_problem.lean
decidable.lean
decl_olean.lean
declare_axiom.lean
def1.lean
def2.lean
def3.lean
def4.lean
def5.lean
def6.lean
def7.lean
def8.lean
def9.lean
def10.lean
def11.lean
def12.lean
def13.lean
def_alias.lean
def_brec1.lean
def_brec2.lean
def_brec3.lean
def_brec4.lean
def_brec_reflexive.lean
def_complete_bug.lean
def_ite1.lean
def_ite_value.lean
defaul_param3.lean
default_field_pi.lean
default_field_universe.lean
default_field_values1.lean
default_param.lean
default_param2.lean
dep_coe_to_fn.lean
dep_coe_to_fn2.lean
dep_coe_to_fn3.lean
dependent_seq.lean fix(init/meta/tactic): skip solved goals in seq_focus and seq 2017-07-21 02:10:48 -07:00
destruct.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
div2.lean feat(library/init/meta/well_founded_tactics): add simple tactic for discharging decreasing proofs 2017-05-23 22:07:46 -07:00
div_wf.lean
do_const_pat.lean fix(frontends/lean/builtin_exprs): allow constant patterns in do notation 2017-07-20 01:51:00 -07:00
do_let_notation.lean
do_match_else.lean
do_notation_tmp_var_issue.lean
doc_string1.lean
doc_string2.lean
doc_string3.lean
doc_string4.lean feat(library/init/meta/interactive): rw [-h] ==> rw [← h] 2017-07-05 11:42:55 -07:00
doc_string5.lean
docstring_after_variables.lean fix(frontends/lean/util): allow docstrings after variables 2017-08-01 10:18:05 +01:00
dsimp_options.lean feat(library/tactic/dsimplify): new configuration options for dsimp 2017-07-02 18:26:03 -07:00
dsimp_partial_app.lean refactor(init/data/list): move out advanced list defs 2017-07-26 11:52:11 +01:00
dsimp_proj.lean feat(library/init/meta/simp_tactic): add option for reducing [reducible] definitions at dsimp, and to_unfold : list name similar to the one in the simp tactic 2017-07-03 13:28:46 -07:00
dsimp_test.lean feat(library/init/meta/interactive): simp without foo ==> simp [-foo] 2017-07-03 17:10:46 -07:00
dsimp_unfold_reducible_bug.lean fix(library/tactic/dsimplify): issue reported by @semorrison at gitter 2017-07-05 21:48:44 -07:00
dsimplify1.lean
dsimplify2.lean
dunfold3.lean feat(library/init/meta/interactive): simp and unfold can unfold projection applications 2017-07-02 16:28:04 -07:00
dunfold4.lean
e1.lean
e2.lean
e3.lean
e4.lean
e5.lean
e15.lean
e16.lean
elab3.lean
elab4.lean
elab5.lean
elab6.lean
elab_bool.lean
elab_crash1.lean
elab_failure.lean
elab_meta1.lean
ematch1.lean
ematch2.lean
ematch_attr_to_defs.lean
ematch_loop.lean
ematch_partial_apps.lean refactor(init/data/list): move out advanced list defs 2017-07-26 11:52:11 +01:00
empty_eq.lean
empty_match.lean
empty_match_bug.lean
empty_set_inside_quotations.lean refactor(*): move out stdlib 2017-07-26 11:52:10 +01:00
emptyc_issue.lean
enum.lean
eq1.lean
eq2.lean
eq4.lean
eq5.lean
eq6.lean
eq9.lean
eq10.lean
eq11.lean
eq12.lean
eq13.lean
eq15.lean
eq16.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
eq17.lean
eq20.lean
eq21.lean
eq22.lean
eq25.lean
eq_cases_on.lean refactor(*): move out stdlib 2017-07-26 11:52:10 +01:00
eq_mpr_def_issue.lean
eqn_compiler_perf_issue.lean
eqn_compiler_perf_issue2.lean fix(library/equations_compiler): performance problem reported by @dselsam 2017-06-27 15:24:12 -07:00
eqn_compiler_variable_or_inaccessible.lean
eqn_issue.lean
eqn_value_issue.lean fix(library/equations_compiler/elim_match): whnf_pattern 2017-05-31 10:02:59 -07:00
equation_with_values.lean
eval_attr_cache.lean
eval_constant.lean
eval_expr_bug.lean
eval_expr_partial.lean
even_odd.lean feat(library/init/meta/interactive): simph ==> simp [*] 2017-07-03 15:14:47 -07:00
even_odd2.lean feat(library/init/meta/interactive): simph ==> simp [*] 2017-07-03 15:14:47 -07:00
even_perf.lean
ex.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
exact_perf.lean
exact_tac1.lean
example1.lean
exfalso1.lean
exhaustive_vm_impl_test.lean feat(tests): test overriden VM functions on small values 2017-07-11 23:00:09 +01:00
exists_intro1.lean
export.lean
export2.lean
fib_wrec.lean refactor(init/data): move out some nat lemmas 2017-07-26 11:52:10 +01:00
find.lean
fingerprint.lean
fn_default.lean
format.lean
full.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
fun.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
fun_info1.lean
funext_issue.lean
gcd.lean
generalize_inst.lean chore(library/standard): remove standard.lean (unused, and confusing given stdlib) 2017-07-28 16:47:53 +01:00
generalizes.lean
ginductive_induction_tactic.lean
ginductive_pred.lean
handthen.lean feat(frontends/lean/tactic_notation): add support for tac ; [tac_1, ..., tac_n] notation in interactive tactic mode 2017-06-02 11:38:04 -07:00
have1.lean
have2.lean
have3.lean chore(frontends/lean): remove then have ... notation 2017-06-19 14:20:52 -07:00
have4.lean chore(frontends/lean): remove then have ... notation 2017-06-19 14:20:52 -07:00
have5.lean feat(frontends/lean/builtin_exprs): support have ... := ... in term mode 2017-07-05 11:20:10 -07:00
have6.lean chore(frontends/lean): remove then have ... notation 2017-06-19 14:20:52 -07:00
heap.lean
help_cmd.lean
hinst_lemma1.lean
hinst_lemmas1.lean
ho.lean
hole1.lean feat(frontends/lean): {! ... !} takes a list of pre-terms 2017-06-13 22:19:17 -07:00
id.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
if_dollar_prec.lean
imp.lean
imp2.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
imp3.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
implicit.lean
include_bug.lean
ind0.lean
ind1.lean
ind2.lean
ind3.lean
ind5.lean
ind6.lean
ind7.lean
ind8.lean
ind_bug.lean
ind_cnst_params.lean
ind_issue.lean
ind_ns.lean
ind_tac1.lean
indbug2.lean
indimp.lean
induction_tac3.lean
induction_tactic_delta.lean
induction_with_drec.lean
inductive_nonrec_after_rec.lean feat(library/init/meta/interactive): unfold is now based on the simp framework 2017-07-02 11:30:48 -07:00
inductive_sorry.lean
inductive_type_whnf.lean fix(kernel/inductive/inductive): identify indices modulo whnf 2017-07-06 20:59:58 -07:00
infix_paren.lean
injection.lean fix(library/constructions/injective): use same transparency setting as no_confusion 2017-06-08 10:17:21 +02:00
injection1.lean
inliner_bug.lean
inst_bug.lean
int_eq_num.lean
interactive1.lean feat(library/init/meta/interactive): simp without foo ==> simp [-foo] 2017-07-03 17:10:46 -07:00
interp.lean
intros_defeq_canonizer_bug.lean
introv.lean feat(library/init/meta/tactic): add dependent parameters for empty introv 2017-05-31 15:10:07 -07:00
IO1.lean
IO2.lean
IO3.lean
IO4.lean
io_fs.lean
io_process_env.lean
io_state.lean
is_def_eq_perf_bug.lean
is_true.lean
isabelle.lean refactor(init/data/list): move out advanced list defs 2017-07-26 11:52:11 +01:00
itac.lean
K_new_elab.lean
kabstract_cache.lean feat(library/init/meta/simp_tactic): add option for reducing [reducible] definitions at dsimp, and to_unfold : list name similar to the one in the simp tactic 2017-07-03 13:28:46 -07:00
kcomp.lean
kdepends_on.lean
kha_inst_bug.lean
lambda_cons.lean
lambda_simp.lean
lamexp.lean
let1.lean
let2.lean
let3.lean
let_vm_bug.lean
level_bug1.lean
level_bug2.lean
level_bug3.lean
lift.lean
lift2.lean
lift_nested_rec.lean
list_mem_pred.lean
list_notation.lean
listex.lean
listex2.lean chore(*): remove super 2017-05-31 10:10:47 -07:00
listex3.lean
listex4.lean
local_notation.lean
local_ns_shadow.lean
lst64.lean perf(frontends/lean): add notation #[...] 2017-07-21 04:20:48 -07:00
match2.lean
match3.lean
match4.lean
match_anonymous_constructor.lean
match_convoy.lean
match_convoy2.lean
match_convoy3.lean
match_expr.lean
match_expr2.lean
match_fun.lean
match_pattern1.lean
match_pattern2.lean
matrix.lean
matrix2.lean
max_memory.lean
mem_nil.lean
meta1.lean
meta2.lean
meta3.lean
meta_env1.lean refactor(*): wrap string in a structure 2017-06-07 17:30:49 -07:00
meta_expr1.lean
meta_level1.lean
meta_tac1.lean
meta_tac2.lean
meta_tac3.lean
meta_tac4.lean
meta_tac5.lean
meta_tac6.lean
meta_tac7.lean
mixed_tmp_non_tmp_universe_bug.lean
mk_byte.lean refactor(library): remove vector and bitvec from init 2017-08-16 13:40:50 -07:00
mk_dec_eq1.lean fix(init/meta/mk_dec_eq_instance): bug for dependent structures 2017-06-25 14:55:47 -07:00
mk_dec_eq_instance_indices.lean fix(init/meta/mk_dec_eq_instance): bug for dependent structures 2017-06-25 14:55:47 -07:00
mk_dec_eq_instance_nested.lean
mk_inhabited1.lean
mk_instance1.lean
monad_univ_lift.lean
mutual_inductive.lean
mutual_parameter.lean fix(frontends/lean/definition_cmds): support parameters in mutual defs 2017-07-13 15:14:46 +01:00
mvar_backtrack.lean
my_tac_class.lean fix(tests/*): fix tests 2017-06-22 08:24:19 -07:00
n3.lean
n5.lean
name_resolution_at_tactic_execution_time.lean
name_resolution_with_params_bug.lean feat(library/init/meta/rewrite_tactic): improve rewrite tactic 2017-06-30 12:03:27 -07:00
namespace_local.lean
nary_existsi.lean feat(library/init/meta/interactive): add nary existsi 2017-05-31 13:41:25 -07:00
nat_bug.lean refactor(frontends/lean/token_table,library): take ~> assume 2017-07-05 11:20:10 -07:00
nat_bug4.lean
nat_bug7.lean
nat_sub_ematch.lean
nateq.lean
nested_begin_end.lean
nested_common_subexpr_issue.lean
nested_inductive.lean
nested_inductive_code_gen.lean
nested_inductive_sizeof.lean feat(inductive_compiler): generate sizeof_spec for nested constructors 2017-05-20 08:30:57 -07:00
new_elab1.lean
new_elab2.lean
new_proj_notation.lean
no_confusion1.lean
no_confusion_bug.lean
no_field_access.lean
noequations.lean fix(library/equations_compiler/util): PR #1731 2017-07-06 21:29:23 -07:00
noncomputable_example.lean
noncomputable_meta.lean
norm_num_tst.lean
not_bug1.lean
ns.lean
ns1.lean
ns2.lean
num.lean
occurs_check_bug1.lean fix(tests/lean): fix tests 2017-06-27 18:55:52 -07:00
offset1.lean
one.lean
one2.lean
opaque_hint_bug.lean
opt1.lean
opt_param_cc.lean
opt_param_cnsts.lean
order_defaults.lean chore(init/algebra/order): typo 2017-08-02 15:41:51 +01:00
over2.lean
over3.lean
over_subst.lean
overload2.lean chore(library/standard): remove standard.lean (unused, and confusing given stdlib) 2017-07-28 16:47:53 +01:00
overload_issue.lean
pack_unpack1.lean
pack_unpack2.lean
pack_unpack3.lean
parent_struct_inst.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
parent_struct_ref.lean
partial_explicit.lean
partial_explicit1.lean
period_after_eqns.lean
pi_patterns.lean
pp_unit.lean
prec_max.lean
pred_to_subtype_coercion.lean
pred_using_structure_cmd.lean
print_inductive.lean
print_poly.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
priority_test.lean
priority_test2.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
private_names.lean
prod_notation.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
proj_unify.lean
protected.lean
psum_wf_rec.lean test(tests/lean/run/psum_wf_rec): add example used on Slack to test suite 2017-05-30 16:59:35 -07:00
ptst.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
qed_perf_bug.lean
qexpr1.lean
quote1.lean
quote_bas.lean feat(library/init/meta/interactive): simph ==> simp [*] 2017-07-03 15:14:47 -07:00
quote_wo_eval.lean fix(library): make sure `(t) does not evaluate t 2017-05-31 22:03:15 -07:00
rb_map1.lean
rec_and_tac_issue.lean
rec_eq_ematch_bug.lean
rec_meta_issue.lean
record1.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
record2.lean
record4.lean
record7.lean
record8.lean
record9.lean
record10.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
reflected.lean
reflected_coercion_with_mvars.lean fix(frontends/lean/elaborator): make sure coercions from (reflected t) to expr fire when t contains metavariables that can be synthesized by type class resolution 2017-05-31 23:33:48 -07:00
reflexive_elim_prop_bug.lean
regset.lean
rel_tac1.lean
reserve.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
resolve_name_bug.lean feat(library/init/meta/interactive): unfold is now based on the simp framework 2017-07-02 11:30:48 -07:00
revert_crash.lean
root.lean
run_tactic1.lean
rvec.lean
rw1.lean feat(library/init/meta/rewrite_tactic): improve rewrite tactic 2017-06-30 12:03:27 -07:00
rw_eqn_lemmas.lean fix(tests/lean): fix tests 2017-06-27 18:55:52 -07:00
rw_set1.lean
rw_set3.lean
rw_set4.lean
sec_bug.lean
sec_notation.lean
sec_var.lean refactor(frontends/lean/token_table,library): take ~> assume 2017-07-05 11:20:10 -07:00
seclvl.lean
secnot.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
section1.lean
section2.lean
section3.lean
section4.lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
section5.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
section_var_bug.lean
set1.lean
set_attr1.lean chore(library/init/meta): add to_unfold parameter to simplify, and remove redundant simp* tactics 2017-07-02 15:26:06 -07:00
shadow1.lean
show_goal.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
sigma_match.lean
simp1.lean
simp_at_bug.lean fix(library/init/meta/interactive): make sure all input hypotheses are simplified before we clear the old ones 2017-07-03 21:58:55 -07:00
simp_attr_eqns.lean
simp_beta.lean
simp_dif.lean fix(library/init/meta/tactic): by_cases tactic 2017-07-02 21:34:10 -07:00
simp_eqns.lean
simp_eta.lean
simp_if_true_false.lean
simp_lemma_issue.lean
simp_lemmas_with_mvars.lean feat(library/tactic/simp_lemmas): simp lemmas may contain metavariables 2017-06-28 18:17:21 -07:00
simp_match_reducibility_issue.lean refactor(library): remove vector and bitvec from init 2017-08-16 13:40:50 -07:00
simp_options.lean fix(tests/lean/*): fix and expand tests 2017-06-04 13:23:26 -07:00
simp_partial_app.lean refactor(init/data/list): move out advanced list defs 2017-07-26 11:52:11 +01:00
simp_proj.lean feat(library/init/meta/interactive): simp_all ==> simp * at * 2017-07-04 11:57:16 -07:00
simp_proof_failure.lean
simp_refl_lemma_perf_issue.lean feat(library/tactic/simplify): store proof for refl lemmas and use them in simp 2017-06-21 16:21:11 -07:00
simp_rfl_proof_issue.lean test(tests/lean/run/simp_rfl_proof_issue): add simp refl proof test 2017-06-05 15:36:26 -07:00
simp_single_pass.lean fix(tests/lean): fix tests 2017-06-27 18:55:52 -07:00
simp_subgoals.lean feat(library/init/meta): allow users to specify tactic for discharging subgoals in the simp tactic family 2017-07-01 15:35:33 -07:00
simp_univ_metavars.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
simp_univ_poly.lean fix(library/tactic/simplify): handle universe polymorphic simplification rules 2017-08-03 17:42:07 +01:00
simple.lean
simplifier_custom_relations.lean chore(library/init/meta): add to_unfold parameter to simplify, and remove redundant simp* tactics 2017-07-02 15:26:06 -07:00
simulate_on.lean feat(library/init/meta/tactic): simplify ‹p› notation 2017-07-07 12:05:02 -07:00
size_of1.lean
sizeof2.lean
slack_eqn_issue.lean
smt_array.lean
smt_assert_define.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
smt_destruct.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
smt_ematch1.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
smt_ematch2.lean
smt_ematch3.lean chore(tests/lean): fix test suite 2017-07-26 14:10:02 +01:00
smt_ematch_alg_issue.lean
smt_facts_as_hinst_lemmas.lean
smt_not_exists.lean
smt_rsimp.lean
smt_tactic.lean feat(frontends/lean/tactic_notation): allow interactive tactics to take itactic arguments from a different tac_class 2017-06-28 14:51:42 -07:00
smt_tests.lean
smt_tests2.lean
smt_tests3.lean chore(init/data/nat): rename add_one_eq_succ -> add_one 2017-07-26 11:52:10 +01:00
sorry.lean
soundness.lean feat(library/init/meta/interactive): simph ==> simp [*] 2017-07-03 15:14:47 -07:00
specialize.lean feat(library/init/meta/interactive): add specialize tactic 2017-08-02 10:20:25 +01:00
stateT1.lean
strict_quoted_name_in_patexpr.lean
struc_names.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
struct_bug1.lean
struct_bug2.lean
struct_bug3.lean
struct_extend_univ.lean
struct_inst_exprs2.lean
struct_value.lean feat(init/meta/attribute,library/tactic/attribute): user_attribute apply handlers 2017-08-02 14:32:39 +01:00
structure_default_value_issue.lean
structure_doc_string.lean
structure_opt_param.lean feat(frontends/lean/structure_cmd): default parameter for structure/class declarations 2017-06-28 12:20:56 -07:00
structure_result_universe.lean
sub.lean
sub_bug.lean
subst_tac1.lean
subst_vars.lean
suffices.lean
sufficies.lean
super.lean
t1.lean
t2.lean fix(frontends/lean/parser): make sure imax and max level arguments are parsed using the same precendence we use to parse application arguments 2017-07-07 12:43:07 -07:00
t3.lean
t4.lean
t5.lean
t6.lean
t7.lean
t9.lean
t10.lean
t11.lean
tactic_io.lean
tactic_mode_scope_bug.lean refactor(frontends/lean/tactic_notation): rename note/define tactics to have/let 2017-06-22 08:03:23 -07:00
tactic_ref.lean feat(library/tactic): add tactic::ref 2017-06-02 15:19:03 -07:00
tc_inout1.lean
tc_loop.lean
term_app.lean fix(library/equations_compiler/util): missing case at prove_eq_rec_invertible 2017-05-24 14:34:54 -07:00
term_app2.lean chore(init/data/nat): rename add_one_eq_succ -> add_one 2017-07-26 11:52:10 +01:00
term_pred.lean feat(library/tactic/cases_tactic): add support for injective functions in the cases tactic 2017-06-07 19:50:01 -07:00
test_all.sh
test_perm_ac1.lean
test_single.sh
thunk_overload.lean
trace_call_stack_segfault.lean
trace_tst.lean
tree_map.lean test(tests/lean/tree_map): closes #1457 2017-05-24 17:15:12 -07:00
try_for1.lean
tuple_head_issue.lean refactor(library): remove vector and bitvec from init 2017-08-16 13:40:50 -07:00
type_equations.lean
u_eq_max_u_v.lean feat(library/tactic/dsimplify): new configuration options for dsimp 2017-07-02 18:26:03 -07:00
unfold_default_values.lean
unfold_issue.lean feat(library/init/meta/interactive): unfold is now based on the simp framework 2017-07-02 11:30:48 -07:00
unfold_lemmas.lean fix(tests/lean): fix tests 2017-06-27 18:55:52 -07:00
uni_issue1.lean
uni_var_bug.lean
unicode.lean
unification_hints.lean
unify_fo_approx_bug1.lean
univ1.lean
univ2.lean
univ_bug1.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
univ_bug2.lean refactor(frontends/lean): do not hard code commands accepting attributes & modifiers 2017-06-19 11:09:26 -07:00
univ_cnstr1.lean
univ_delay_thm_bug.lean
univ_elab_issue.lean
unreachable_cases.lean
untrusted_examples.lean
user_simp_attributes.lean
using_smt1.lean feat(library/tactic/dsimplify): new configuration options for dsimp 2017-07-02 18:26:03 -07:00
using_smt2.lean
using_smt3.lean
vars_anywhere.lean
vector2.lean chore(tests/lean): fix test suite 2017-07-26 14:10:02 +01:00
vector3.lean chore(tests/lean): fix test suite 2017-07-26 14:10:02 +01:00
vm_check_bug.lean
vm_eval1.lean
wfrec1.lean refactor(library/init/data/sigma/lex): define psigma.lex 2017-05-23 20:39:09 -07:00
whenIO.lean
whnf_mvar.lean test(tests/lean/run/whnf_mvar): add test to check whether whnf instantiate mvars or not 2017-08-03 11:29:22 +01:00
whnfinst.lean
with_update_class.lean
xrewrite1.lean feat(library/init/meta/rewrite_tactic): improve rewrite tactic 2017-06-30 12:03:27 -07:00