Leonardo de Moura 21c41f50ea fix(frontends/lean/elaborator): fixes #803		2015-08-17 14:56:41 -07:00
..
252.lean	feat(frontends/lean/coercion_elaborator): "coercion lifting" for backtracking case	2015-05-30 16:44:26 -07:00
331.lean
360_1.lean
361.lean
362.lean
415.hlean
444.lean
445.lean
454.lean
466.lean
490.lean
505.lean
511a.lean	feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants	2015-05-27 16:32:43 -07:00
541a.lean	feat(nat): redefine le and lt in the standard library	2015-06-04 20:14:13 -04:00
541b.lean	test(tests/lean/run): add examples showing how to prove (using tactics) that direct_subterm relation is well-founded	2015-06-09 16:17:29 -07:00
543.lean
548.lean
567.lean
568.lean
570.lean
570b.lean
585.lean	refactor(logic/funext.lean, algebra/function.lean): delete logic/funext, merge into algebra/function	2015-05-23 16:16:36 +10:00
588.lean
592.lean
600a.lean
600b.lean
600c.lean
645a.lean	feat(library/tactic): automate "generalize-intro-induction/cases" idiom	2015-05-30 21:57:28 -07:00
662.lean	fix(library/unifier): try to generate approximate solution for flex-flex constraints before discarding them	2015-06-09 14:36:31 -07:00
662b.lean	test(tests/lean/run): add test/example	2015-06-09 14:50:15 -07:00
668.lean	test(tests/lean/run): add test showing new coercion module addresses issue #668	2015-07-01 16:41:19 -07:00
676.lean	feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic	2015-06-17 23:48:54 -07:00
679a.lean	feat(library/class): allow any constant to be marked as a class	2015-06-17 16:26:45 -07:00
679b.lean	feat(library/class): allow any constant to be marked as a class	2015-06-17 16:26:45 -07:00
682.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
687.lean	fix(frontends/lean/elaborator): fixes #687	2015-06-28 19:58:57 -07:00
695d.lean	feat(frontends/lean/parse_rewrite_tactic): accept trailing comman in rewrite tactic	2015-06-28 11:45:30 -07:00
695e.lean	test(tests/lean/run): add test for <d notation	2015-06-28 13:10:15 -07:00
702.lean	fix(library/tactic/rewrite_tactic): fixes #702	2015-06-28 20:37:17 -07:00
724.lean	fix(frontends/lean/elaborator): fixes #724	2015-07-06 15:19:19 -07:00
751.lean	fix(library/util): fixes #751	2015-07-28 16:30:20 -07:00
774.lean	feat(frontends/lean/decl_cmds): allow recursive examples	2015-08-08 08:26:25 -07:00
791.lean	feat(frontends/lean/decl_cmds): closes #791	2015-08-11 17:53:33 -07:00
796.lean	fix(library/definitional/equations): fixes #796	2015-08-14 14:39:23 -07:00
801.lean	fix(library/normalize): fixes #801	2015-08-16 14:22:02 -07:00
803.lean	fix(frontends/lean/elaborator): fixes #803	2015-08-17 14:56:41 -07:00
abs.lean
ack.lean
alg_rw.lean
algebra1.lean
algebra3.lean
alias1.lean
alias2.lean
alias3.lean
all_goals.lean	feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'	2015-07-07 16:37:06 -07:00
all_goals2.lean	feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'	2015-07-07 16:37:06 -07:00
app_builder.lean
apply_class_issue0.lean
as.lean
assert_tac.lean
assert_tac2.lean
atomic2.lean
atomic_notation.lean
attrs.lean
basic.lean
begin_end_plus.lean
beginend.lean
beginend3.lean
booltst.lean
bquant.lean
bug5.lean
bug6.lean
by_exact.lean
calc.lean
calc_auto_trans_eq.lean	fix(tests): update tests to reflect the change of notation from \~ to ~	2015-06-25 22:55:05 -04:00
calc_bug.lean
calc_heq_symm.lean
calc_imp.lean
cases_bug.lean
cast_sorry_bug.lean
choice_ctx.lean
choose_test.lean
class1.lean
class2.lean
class3.lean
class4.lean
class5.lean
class6.lean
class7.lean
class8.lean
class11.lean
class_bug1.lean
class_bug2.lean
class_coe.lean
clear_tac.lean
clears_tac.lean
cody1.lean
cody2.lean
coe1.lean
coe2.lean
coe3.lean
coe4.lean
coe5.lean
coe6.lean
coe7.lean
coe8.lean
coe9.lean
coe10.lean
coe11.lean
coe12.lean
coe13.lean
coe14.lean
coe15.lean
coefun.lean
coercion_bug.lean
coercion_bug2.lean
coesec.lean
comment.lean
confuse_ind.lean
congr.lean	feat(frontends/lean/bultin_cmds): add 'print [congr]' command for displaying active congruence rules	2015-07-23 18:52:59 -07:00
congr_imp_bug.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
congr_tac.lean
congr_tac2.lean	feat(library/tactic/congruence_tactic): add congruence lemma generator	2015-06-05 22:00:10 -07:00
const_choice.lean
constr_tac.lean
constr_tac2.lean
constr_tac3.lean
constr_tac4.lean	feat(nat): redefine le and lt in the standard library	2015-06-04 20:14:13 -04:00
consume.lean
contra1.lean
contra2.lean	feat(library/tactic/contradiction_tactic): handle (h1 : p) and (h2 : not p) hypotheses in the contradiction tactic	2015-05-25 10:29:51 -07:00
ctx.lean
dec_trivial_loop.lean
deceq_vec.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
decidable.lean
def_tac.lean
dep_subst.lean	fix(library/tactic/subst_tactic): in the standard mode, use dependent elimination in the subst tactic (when needed)	2015-06-03 17:36:04 -07:00
dfun_tst.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
diag.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
div2.lean	feat(frontends/lean): add simp tactic frontend stub	2015-07-14 09:54:53 -04:00
div_wf.lean
e1.lean
e2.lean
e3.lean
e4.lean
e5.lean
e6.lean
e7.lean
e8.lean
e9.lean
e10.lean
e11.lean
e12.lean
e13.lean
e14.lean
e15.lean
e16.lean
e17.lean
e18.lean
eassumption.lean	feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic	2015-06-17 23:48:54 -07:00
elab_bug1.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
elab_failure.lean
elim.lean
elim2.lean
empty_eq.lean	refactor(library/data): replace 'fin' with Haitao's 'less_than'	2015-06-05 10:33:19 -07:00
empty_match.lean
empty_match_bug.lean	refactor(library/data): replace 'fin' with Haitao's 'less_than'	2015-06-05 10:33:19 -07:00
enum.lean
eq1.lean
eq2.lean
eq3.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
eq4.lean
eq5.lean
eq6.lean
eq7.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
eq8.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
eq9.lean
eq10.lean
eq11.lean
eq12.lean
eq13.lean
eq14.lean
eq15.lean
eq16.lean
eq17.lean
eq18.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
eq19.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
eq20.lean
eq21.lean
eq22.lean
eq23.lean
eq24.lean
eq25.lean
eqn_tac.lean
eqv_tacs.lean
esimp1.lean	feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function	2015-07-08 21:19:18 -04:00
ex.lean
example1.lean
exfalso1.lean
export.lean
export2.lean
fapply.lean
fib_brec.lean	feat(datatypes): let the type of unit be the lowest non-Prop universe	2015-06-25 17:33:46 -07:00
fib_wrec.lean
fibrant_class1.lean	feat(library): add 'noncomputable' keyword for the standard library	2015-07-28 21:56:35 -07:00
fibrant_class2.lean	feat(library): add 'noncomputable' keyword for the standard library	2015-07-28 21:56:35 -07:00
finbug.lean	refactor(library/*): remove 'Module:' lines	2015-05-23 20:52:23 +10:00
finbug2.lean	refactor(library/*): remove 'Module:' lines	2015-05-23 20:52:23 +10:00
find_cmd.lean
finset.lean	fix(tests/lean/run/finset): adjust test to recent changes to the	2015-07-19 11:53:21 -07:00
finset1.lean
finset_coe.lean	feat(frontends/lean/elaborator): use custom normalizers for detecting whether there are coercions from/to a given type	2015-05-20 16:12:12 -07:00
fold.lean
forest.lean	feat(datatypes): let the type of unit be the lowest non-Prop universe	2015-06-25 17:33:46 -07:00
forest2.lean
forest_height.lean	fix(tests/lean): adjust tests to recent changes to the standard library	2015-07-19 21:32:42 -07:00
ftree_brec.lean	feat(datatypes): let the type of unit be the lowest non-Prop universe	2015-06-25 17:33:46 -07:00
full.lean
fun.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
gcd.lean
generalizes.lean
goal.lean
group.lean
group2.lean
group3.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
group4.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
group5.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
group6.lean
hash.lean
have1.lean
have2.lean
have3.lean
have4.lean
have5.lean
have6.lean
help_cmd.lean
ho.lean
id.lean
iff_rw.lean
imp.lean
imp2.lean
imp3.lean
imp_curly.lean
impbug1.lean
impbug2.lean
impbug3.lean
impbug4.lean
implicit.lean
ind0.lean
ind1.lean
ind2.lean
ind3.lean
ind4.lean
ind5.lean
ind6.lean
ind7.lean
ind8.lean
ind_bug.lean
ind_ns.lean
ind_tac.lean
ind_tac1.lean
indbug2.lean
indimp.lean
induction_tac1.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
induction_tac2.lean
induniv.lean
inf_tree.lean	test(tests/lean/run): add examples showing how to prove (using tactics) that direct_subterm relation is well-founded	2015-06-09 16:17:29 -07:00
inf_tree2.lean
inf_tree3.lean
inj_tac.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
injective_decidable.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
inst_bug.lean
interp.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
intros.lean
inv_bug.lean
inv_bug2.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
inversion1.lean	refactor(library/data): replace 'fin' with Haitao's 'less_than'	2015-06-05 10:33:19 -07:00
is_nil.lean	feat(library/inductive_unifier_plugin): restrict rule that was generating non-terminating behavior	2015-05-27 14:41:12 -07:00
is_true.lean
issue332.lean
kcomp.lean
let1.lean
let2.lean
let_tac.lean
level_bug1.lean
level_bug2.lean
level_bug3.lean
lift.lean
lift2.lean
list_elab1.lean
list_vector_overload.lean	feat(frontends/lean): allow user to overload notation containing foldr/foldl and/or scoped expressions	2015-08-16 18:24:30 -07:00
local_eqns.lean
local_eqns2.lean	refactor(library/data): replace 'fin' with Haitao's 'less_than'	2015-06-05 10:33:19 -07:00
local_notation.lean
local_using.lean
localcoe.lean
match1.lean	feat(library): add idx_metavar module	2015-06-08 16:02:37 -07:00
match2.lean	feat(library): add idx_metavar module	2015-06-08 16:02:37 -07:00
match3.lean
match4.lean
match_fun.lean
match_tac.lean
match_tac2.lean
match_tac3.lean
match_tac4.lean
matrix.lean
matrix2.lean
max_memory.lean
measurable.lean
meta.lean
mul_zero.lean
n1.lean
n2.lean
n3.lean
n4.lean
n5.lean
namespace_local.lean
nat_bug.lean
nat_bug2.lean
nat_bug3.lean
nat_bug4.lean
nat_bug5.lean
nat_bug6.lean
nat_bug7.lean
nat_coe.lean
nateq.lean
nested_begin.lean
nested_begin_end.lean
nested_rec.lean	fix(tests/lean): adjust tests to reflect changes in the elaboration process	2015-06-26 17:18:30 -07:00
new_obtain3.lean	fix(tests/lean): fix three tests broken by setext renaming	2015-08-09 22:14:25 -04:00
new_obtain4.lean	fix(tests/lean): fix three tests broken by setext renaming	2015-08-09 22:14:25 -04:00
new_obtains.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
new_obtains2.lean
no_confusion_bug.lean
not_bug1.lean
notation_priority.lean	feat(frontends/lean/util): remove hack that overrides priority namespace	2015-08-11 18:01:40 -07:00
ns.lean
ns1.lean
ns2.lean
num.lean
num_bug2.lean
num_sub.lean
obtain_tac.lean	feat(frontends/lean/builtin_exprs): allow 'obtain' to be used in tactic mode	2015-05-19 16:26:02 -07:00
occurs_check_bug1.lean
one.lean
one2.lean
opaque_hint_bug.lean
over2.lean
over_subst.lean
override1.lean	feat(frontends/lean): add 'override' (notation) command	2015-05-20 11:42:16 -07:00
override_on_equations.lean
parent_struct_ref.lean
parity.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
pickle1.lean
ppbeta.lean
pquot.lean
prec_max.lean
premises.lean
print.lean
print_inductive.lean
print_poly.lean	refactor(library/logic): move logic/choice.lean to init/classical.lean	2015-08-12 18:37:33 -07:00
priority_test.lean	feat(frontends/lean/util): remove hack that overrides priority namespace	2015-08-11 18:01:40 -07:00
priority_test2.lean	feat(frontends/lean/util): remove hack that overrides priority namespace	2015-08-11 18:01:40 -07:00
private_names.lean
prod_notation.lean
proj.lean
proof_qed_improved.lean
proof_qed_nested_tac.lean
protected.lean
ptst.lean
rat_coe.lean	feat(frontends/lean/elaborator): use custom normalizers for detecting whether there are coercions from/to a given type	2015-05-20 16:12:12 -07:00
rat_rfl.lean	feat(frontends/lean/builtin_cmds): do not unfold proofs in the eval command	2015-05-20 19:14:57 -07:00
record1.lean
record2.lean
record3.lean
record4.lean
record5.lean
record6.lean
record7.lean
record8.lean
record9.lean
record10.lean
reducible.lean
refine1.lean
refine2.lean
refine3.lean
refl_beta.lean	fix(library/tactic/relation_tactics): beta-reduce goal before trying to extract head symbol	2015-05-24 18:56:35 -07:00
rel.lean
rename_tac.lean
reserve.lean
revert_tac.lean
reverts_tac.lean
rewrite4.lean
rewrite5.lean
rewrite8.lean
rewrite9.lean
rewrite10.lean	fix(tests): to reflect recent changes in the standard library	2015-07-06 15:05:01 -07:00
rewrite12.lean
rewrite_bug.lean
rewrite_with_beta.lean	fix(library/tactic/relation_tactics): beta-reduce goal before trying to extract head symbol	2015-05-24 18:56:35 -07:00
rewriter1.lean
rewriter2.lean
rewriter3.lean
rewriter6.lean
rewriter7.lean
rewriter11.lean
rewriter12.lean
rewriter13.lean
rewriter14.lean	feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'	2015-07-07 16:37:06 -07:00
rewriter15.lean
rewriter16.lean
rewriter17.lean
rewriter18.lean
root.lean
rw_bug2.lean
rw_set1.lean	feat(frontends/lean,library): rename '[rewrite]' to '[simp]'	2015-07-22 09:01:42 -07:00
rw_set2.lean	feat(library/simplifier): add API for extracting simplification rules defined in a given namespace	2015-07-22 18:47:56 -07:00
scope_bug.lean
sec_bug.lean
sec_notation.lean
sec_var.lean
seclvl.lean
secnot.lean
section1.lean
section2.lean
section3.lean
section4.lean
section5.lean
set.lean
set2.lean
show2.lean	feat(frontends/lean/builtin_exprs): rename 'show' hidden name to 'this'	2015-08-07 13:29:21 -07:00
sigma_match.lean
sigma_no_confusion.lean
simple.lean
sorry.lean
soundness.lean	feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic	2015-06-17 23:48:54 -07:00
st_options.lean
string.lean
struc_names.lean
struct_bug1.lean
struct_infer.lean
struct_inst_exprs.lean	refactor(library/init): define prod as an inductive datatype	2015-06-25 17:59:06 -07:00
struct_inst_exprs2.lean
structure_test.lean
sub.lean	refactor(library/logic): move logic/choice.lean to init/classical.lean	2015-08-12 18:37:33 -07:00
sub_bug.lean	refactor(library/logic): move logic/choice.lean to init/classical.lean	2015-08-12 18:37:33 -07:00
subst_tact.lean
subst_test.lean	feat(frontends/lean/elaborator): hide auxiliary 'match' hypothesis during elaboration	2015-05-25 15:24:56 -07:00
subst_test2.lean	test(tests/lean/run): add missing test	2015-05-25 17:02:23 -07:00
sum_bug.lean
t1.lean
t2.lean
t3.lean
t4.lean
t5.lean
t6.lean
t7.lean
t8.lean
t9.lean
t10.lean
t11.lean
tac1.lean
tactic1.lean
tactic2.lean
tactic3.lean
tactic4.lean
tactic5.lean
tactic6.lean
tactic7.lean
tactic8.lean
tactic9.lean
tactic10.lean
tactic11.lean
tactic12.lean
tactic13.lean
tactic14.lean
tactic15.lean
tactic16.lean
tactic17.lean
tactic18.lean
tactic19.lean
tactic20.lean
tactic21.lean
tactic22.lean
tactic23.lean	feat(library/inductive_unifier_plugin): restrict rule that was generating non-terminating behavior	2015-05-27 14:41:12 -07:00
tactic24.lean
tactic25.lean
tactic26.lean	feat(library): add 'noncomputable' keyword for the standard library	2015-07-28 21:56:35 -07:00
tactic27.lean
tactic28.lean	feat(library): add 'noncomputable' keyword for the standard library	2015-07-28 21:56:35 -07:00
tactic29.lean
tactic30.lean
tactic31.lean
tactic_notation.lean
tactic_op_overload_bug.lean
tele_eq.lean
test_single.sh
trans.lean
tree.lean	feat(datatypes): let the type of unit be the lowest non-Prop universe	2015-06-25 17:33:46 -07:00
tree2.lean
tree3.lean
tree_height.lean
tree_subterm_pred.lean	test(tests/lean/run): add examples showing how to prove (using tactics) that direct_subterm relation is well-founded	2015-06-09 16:17:29 -07:00
trick.lean
true_imp_rw.lean
tt1.lean
tut_104.lean	feat(library/*): add theorems from Haitao on sets and functions, clean up	2015-06-04 11:55:25 -07:00
type_equations.lean	test(tests/lean/run): add examples showing how to prove (using tactics) that direct_subterm relation is well-founded	2015-06-09 16:17:29 -07:00
unfold_rec.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
unfold_rec2.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
unfold_tac_bug1.lean	fix(library/tactic/unfold_rec): add annother brec pattern that should be checked in the unfold recursive definition tactic	2015-07-10 22:16:23 -04:00
unfold_test.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
uni_issue1.lean
uni_var_bug.lean
unicode.lean
univ1.lean
univ2.lean
univ_bug1.lean	feat(frontends/lean): add simp tactic frontend stub	2015-07-14 09:54:53 -04:00
univ_bug2.lean
univ_problem.lean	feat(datatypes): let the type of unit be the lowest non-Prop universe	2015-06-25 17:33:46 -07:00
univs.lean
unzip_bug.lean	refactor(library/data): move vector as indexed family to examples folder	2015-08-12 15:05:14 -07:00
using_bug.lean
using_bug2.lean
using_expr.lean
uuu.lean
vars_anywhere.lean
vec_inv.lean
vec_inv2.lean
vec_inv3.lean
vector.lean	feat(datatypes): let the type of unit be the lowest non-Prop universe	2015-06-25 17:33:46 -07:00
vector2.lean
vector3.lean
vector_subterm_pred.lean	test(tests/lean/run): add examples showing how to prove (using tactics) that direct_subterm relation is well-founded	2015-06-09 16:17:29 -07:00
whnfinst.lean