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 e4b3dee526 feat(library/simplify): use custom matcher in the simplifier, and remove hack from type_context 
@joehendrix This commit is implementing the matcher that postpones
implicit arguments. The lemma get_data_mk_byte can be proved without
using any hacks in the type_context unifier.

I also added the trace class: simplify.implicit_failure
If we use the command

   set_option trace.simplify.implicit_failure true

Then, the simplifier will generate a diagnostic message every time it
succeeds in the explicit part, but fails in the implicit one.

Please feel free to suggest a better name to his option.

BTW, we can now easily extend the matcher with additional features.
I'm wondering if we will eventually want to write some of these
extensions in Lean.
2017-02-08 22:24:13 -08:00
..
252.lean
331.lean
444.lean
445.lean
490.lean
600a.lean
600b.lean
600c.lean feat(library,frontends/lean): add basic doc string support 2016-11-25 18:52:56 -08:00
662.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
751.lean
774.lean fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
791.lean
808.lean
817.lean
967.lean
968.lean feat(frontends/lean): anonymous instances 2016-09-23 13:34:34 -07:00
1089.lean chore(tests/lean/run/1089): fix test 2016-12-02 16:47:24 -08:00
1093.lean refactor(library/tactic/simplify): delete old simplifier 2016-10-19 14:03:14 -07:00
1163.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
1171.lean fix(library/equations_compiler/elim_match): fixes #1171 2016-10-31 17:42:39 +08:00
1208.lean feat(library/tactic): add "approximate" parameter to apply_core and rewrite_core 2016-12-10 10:24:05 -08:00
1216.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
1218.lean test(tests/lean/run): add test for @1218 2016-12-08 14:10:47 -08:00
1226.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
1253.lean fix(frontends/lean/definition_cmds): bug at inline_new_defs 2016-12-15 20:32:06 -08:00
1258.lean fix(library/type_context): issue #1258 again 2016-12-22 10:51:16 -08:00
1260.lean fix(library/tactic/change_tactic): use id_locked in the change tactic to create checkpoint 2016-12-21 11:29:03 -08:00
1295.lean fix(library/type_context): fix #1295 2017-01-10 11:54:38 -08:00
1302.lean fix(library/compiler/comp_irrelevant): fix #1302 2017-01-11 11:10:17 -08:00
1315a.lean fix(library/equations_compiler/compiler): fix #1315 2017-01-16 20:01:25 -08:00
1315b.lean fix(library/equations_compiler/elim_match): avoid nasty inferred types in auxiliary declarations produced by the equation compiler 2017-01-16 22:55:12 -08:00
1318.lean fix(library/equations_compiler/elim_match): fix #1318 2017-01-18 08:21:53 -08:00
1331.lean feat(library/init/meta): add 'delta' tactic for applying delta reduction 2017-01-26 19:04:07 -08:00
1335.lean fix(library/type_context): assertion violation 2017-01-25 16:05:23 -08:00
abstract_tac.lean feat(library/init/meta): add add_aux_decl and abstract tactics 2017-02-05 16:00:47 -08:00
ac_refl1.lean test(tests/lean/run): add ac_refl tests 2016-12-29 19:51:18 -08:00
ack.lean
add_semi.lean test(tests/lean/run): add test for additive fragment 2016-11-05 11:47:43 -07:00
aexp.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
all_goals1.lean
anonymous_param.lean feat(frontends/lean/parser): add support for anonymous parameters 2016-12-10 11:07:58 -08:00
any_goals.lean feat(library/init/meta): add any_goals tactic 2017-02-06 16:23:29 -08:00
app_builder_tac1.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
apply1.lean
apply2.lean
apply3.lean
apply4.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
arity1.lean refactor(library/init/bool): put main operations in the top-level 2016-09-25 13:32:15 -07:00
as.lean
assert_tac1.lean feat(frontends/lean/tactic_notation, library/init/meta/interactive): add "interactive" versions of define/assert/definev/assertv/note tactics 2016-09-29 18:48:32 -07:00
assert_tac3.lean refactor(library/init/meta/tactic): switch 'pose' and 'note' 2016-12-08 13:17:42 -08:00
assoc_flat.lean chore(library/init/meta): cleanup 2017-02-08 15:33:25 -08:00
at_at_bug.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
atomic2.lean
atomic_notation.lean
auto_eq_congr_extra_args.lean fix(library/tactic/simplify): only use auto_eq_congr if number of args match 2016-11-04 10:13:02 -07:00
auto_propext.lean feat(library/tactic/simplify): use propext in rewriting rules when simplify_config.use_axioms is tt 2016-10-19 17:59:01 -07:00
auto_quote1.lean feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -08:00
back_chaining1.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
back_chaining2.lean feat(frontends/lean): 'by' is now also using interactive mode syntax 2016-09-29 01:57:40 -07:00
back_chaining3.lean feat(frontends/lean): 'by' is now also using interactive mode syntax 2016-09-29 01:57:40 -07:00
back_chaining4.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
basic.lean feat(frontends/lean/definition_cmds): generate equational lemmas for regular definitions that were elaborated without using the equation compiler 2017-01-05 18:02:14 -08:00
basic_monitor.lean feat(frontends/lean, library/init): add 'thunk' gadget 2017-01-31 18:41:59 -08:00
basic_monitor1.lean feat(frontends/lean, library/init): add 'thunk' gadget 2017-01-31 18:41:59 -08:00
basic_monitor2.lean feat(frontends/lean, library/init): add 'thunk' gadget 2017-01-31 18:41:59 -08:00
basic_monitor3.lean fix(library/vm/vm): curr_fn() may not be available 2017-01-12 11:47:45 -08:00
begin_end1.lean feat(frontends/lean): add very basic 'begin ... end' block support 2016-09-24 21:27:27 -07:00
begin_end_do.lean feat(frontends/lean/tactic_notation): do is tactic unit in begin end blocks. 2016-09-30 16:35:45 -07:00
beta_zeta.lean feat(library/init/meta/tactic): add beta/zeta tactics 2016-10-13 18:47:27 -07:00
bin_oct_hex.lean feat(frontends/lean): support binary, octal and hex literals 2016-10-19 10:13:24 -07:00
blast_unit.lean test(tests/lean/run/blast_unit): add old blast unit propagation tests 2017-01-02 19:38:31 -08:00
blast_unit2.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
booltst.lean
bor_lazy.lean feat(frontends/lean, library/init): add 'thunk' gadget 2017-01-31 18:41:59 -08:00
bug5.lean
bug6.lean
bug_proving_eqn_lemmas.lean fix(library/equations_compiler/structural_rec): bug when synthesizing equational lemmas 2017-01-30 11:51:07 -08:00
calc.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
calc_auto_trans_eq.lean
calc_bug.lean
calc_heq_symm.lean feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction 2016-11-29 11:12:43 -08:00
calc_imp.lean
calc_tac.lean chore(tests/lean): adjust tests 2016-10-01 12:57:56 -07:00
cases_bug.lean
cases_bug2.lean
cases_bug3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
cases_crash1.lean
cases_tac1.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
cast_sorry_bug.lean
cc1.lean chore(tests/lean/run): fix tests 2017-01-17 15:50:54 -08:00
cc2.lean fix(library/tactic/congruence/congruence_closure): heq bug and add more tests 2016-12-23 21:57:49 -08:00
cc3.lean fix(library/tactic/congruence/congruence_closure): heq bug and add more tests 2016-12-23 21:57:49 -08:00
cc4.lean fix(library/tactic/congruence/congruence_closure): check_eq_true 2016-12-23 22:24:39 -08:00
cc5.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
cc6.lean test(tests/lean/run/cc6): add more cc tests 2016-12-24 08:50:51 -08:00
cc7.lean fix(library/tactic/congruence/congruence_closure): proof generation for congruence with different arity 2016-12-24 09:12:10 -08:00
cc_ac1.lean feat(library/tactic/congruence/theory_ac): add collapse transition 2016-12-29 11:24:36 -08:00
cc_ac2.lean feat(library/tactic/congruence/theory_ac): add collapse transition 2016-12-29 11:24:36 -08:00
cc_ac3.lean test(tests/lean/run/cc_ac3): add test that requires superpose 2016-12-29 15:11:33 -08:00
cc_ac4.lean test(tests/lean/run): add new AC test with set union 2016-12-29 15:30:29 -08:00
cc_ac5.lean fix(library/tactic/ac_tactics,library/tactic/congruence/theory_ac): crash when mixing different AC symbols 2016-12-29 18:38:40 -08:00
cc_ac_bug.lean fix(library/tactic/congruence/congruence_closure): bug in the interface between cc and ac modules 2016-12-29 19:25:29 -08:00
cc_beta.lean feat(library/tactic/smt/congruence_closure): improve propagation for beta reduction in the congruence closure module 2017-01-24 12:09:37 -08:00
cc_constructors.lean fix(library/tactic/congruence/congruence_closure): crash when processing partially applied constructors 2016-12-26 18:51:03 -08:00
cc_proj.lean feat(library/tactic/congruence/congruence_closure): propagate projection over constructor equality 2016-12-26 19:47:29 -08:00
cc_value.lean feat(library/tactic/congruence/congruence_closure): interpreted values in the same equivalence class 2016-12-25 11:09:55 -08:00
cdcl_examples.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
cheap_try_refl.lean feat(library/init/meta): use cheap "reflexivity" after simp and rewrite 2016-12-08 14:41:26 -08:00
choice_ctx.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
class1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
class2.lean feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction 2016-11-29 11:12:43 -08:00
class3.lean feat(kernel/declaration,*): all theorems are delayed, and are revealed on delta-reduction 2016-11-29 11:12:43 -08:00
class6.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
class11.lean
cody2.lean
coe_opt.lean feat(library/init/coe): add coercion from A to (option A) 2017-01-31 17:45:41 -08:00
coe_univ_bug.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
comment.lean
comp_val1.lean feat(library/init/meta/comp_value_tactics): add comp_val tactic for testing 2016-11-22 17:03:21 -08:00
comp_val2.lean feat(library/init/meta/comp_value_tactics): add support for char/string/fin at comp_val tactic 2016-11-23 13:19:54 -08:00
comp_val3.lean feat(library): add mk_int_val_ne_proof 2016-12-24 15:22:31 -08:00
comp_val4.lean fix(library/comp_val): mk_int_val_ne_proof 2016-12-24 15:54:48 -08:00
compiler_bug1.lean fix(library/compiler/elim_recursors): some recursor applications were not being eliminated 2016-11-02 13:05:52 -07:00
compiler_bug2.lean fix(library/compiler/lambda_lifting): make sure constructors are eta-expanded 2016-11-02 13:26:15 -07:00
compiler_bug3.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
confuse_ind.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
congr_lemma1.lean chore(tests/lean): fix tests 2017-01-20 20:35:18 -08:00
const_choice.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
constructor1.lean
consume.lean
contra1.lean
contra2.lean
contra3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
converter.lean fix(tests/lean/run/converter): fix test 2017-01-16 19:04:52 -08:00
cute_binders.lean feat(frontends/lean): change subtype notation (again) 2016-09-21 17:02:18 -07:00
dec_trivial_problem.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
decidable.lean
decl_olean.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
declare_axiom.lean fix(library/compiler/vm_compiler): prevent segfault 2016-11-04 09:47:17 -07:00
def1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def2.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def5.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def6.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def7.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def8.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def9.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def10.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def11.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def12.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def13.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_alias.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_brec1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_brec2.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_brec3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_brec4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_brec_reflexive.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_complete_bug.lean feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08:00
def_ite1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
def_ite_value.lean feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08:00
defaul_param3.lean test(tests/lean/run/defaul_param3): more tests for default param values 2017-01-31 15:28:06 -08:00
default_field_pi.lean fix(frontends/lean/structure_cmd): default field values of Pi type 2017-01-26 18:53:55 +01:00
default_field_universe.lean fix(frontends/lean/structure_cmd): fix default field values referencing universe variables 2017-01-26 18:52:20 +01:00
default_field_values1.lean feat(frontends/lean): add default field values 2017-01-22 21:25:49 -08:00
default_param.lean feat(frontends/lean/elaborator): default parameter prototype 2017-01-27 16:32:22 -08:00
default_param2.lean feat(frontends/lean): nicer syntax for default parameter values 2017-01-30 15:54:26 -08:00
dep_coe_to_fn.lean feat(library/init/coe,frontends/lean): more general coercions to fun 2016-09-27 15:41:06 -07:00
dep_coe_to_fn2.lean test(tests/lean/run): add more tests for coercion to function 2016-09-27 16:10:50 -07:00
dep_coe_to_fn3.lean feat(tests/lean/run/dep_coe_to_fn3): another dep fn coe test 2016-09-28 09:34:51 -07:00
destruct.lean fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching 2017-01-21 22:38:17 -08:00
div_wf.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
do_match_else.lean feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class 2016-09-29 17:56:35 -07:00
doc_string1.lean chore(frontends/lean): remove namespace documentation 2016-11-27 11:57:03 -08:00
doc_string2.lean chore(frontends/lean): remove namespace documentation 2016-11-27 11:57:03 -08:00
doc_string3.lean feat(frontends/lean): basic leandoc tool 2016-11-27 14:31:31 -08:00
doc_string4.lean feat(shell/leandoc): add support for "brief" description 2016-11-27 21:42:05 -08:00
doc_string5.lean fix(frontends/lean): doc strings after constants and axioms 2017-01-12 00:22:37 -08:00
dsimp_at1.lean feat(library/init/meta): rename rsimp* back to dsimp* 2016-10-11 16:37:08 -07:00
dsimp_partial_app.lean fix(library/tactic/simp_lemmas): refl_lemma_rewrite, make sure a partially applied lhs can be used rewrite terms with "more arguments" 2017-01-23 19:37:35 -08:00
dsimp_test.lean feat(library/init/meta): improve dsimp tactic notation 2017-01-09 17:31:35 -08:00
dsimplify1.lean feat(library/tactic): expose new dsimplify in Lean 2016-10-12 07:25:09 -07:00
dsimplify2.lean feat(library/tactic/simp_lemmas_tactics): add simp_lemmas.drewrite 2016-10-12 09:01:47 -07:00
dunfold1.lean feat(library/tactic/unfold_tactic): add unfold_projection tactic 2016-10-12 13:43:32 -07:00
dunfold2.lean feat(library/tactic/unfold_tactic): allow user to set transparency_mode at dunfold_expr 2016-10-12 14:07:50 -07:00
dunfold3.lean feat(library/init/meta): implement unfold tactics in Lean using new building blocks 2016-10-12 17:25:56 -07:00
dunfold4.lean fix(library/tactic/tactic_state): include implicitly opened namespaces in opened_namespaces 2016-12-18 23:49:00 -08:00
e1.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
e2.lean
e3.lean feat(frontends/lean/definition_cmds): generate equational lemmas for regular definitions that were elaborated without using the equation compiler 2017-01-05 18:02:14 -08:00
e4.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
e5.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
e15.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
e16.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
elab3.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
elab4.lean
elab5.lean
elab6.lean
elab_bool.lean
elab_crash1.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
elab_failure.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
elab_meta1.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
ematch1.lean refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
ematch2.lean refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
ematch_attr_to_defs.lean feat(library/init/meta/smt/ematch): convenient way of marking all equational lemmas of a giving definition as ematch lemmas 2017-01-13 10:35:09 -08:00
ematch_loop.lean feat(library/tactic/smt): add generation heuristic to control matching loops 2017-01-24 22:46:45 -08:00
ematch_partial_apps.lean fix(library/tactic/smt): make sure a partially applied terms can be used to ematch terms with "more arguments" 2017-01-24 19:25:00 -08:00
empty_eq.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
empty_match.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
empty_match_bug.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
empty_set_inside_quotations.lean fix(frontends/lean/elaborator): '{}' inside quotations 2017-02-08 17:50:17 -08:00
enum.lean
eq1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq2.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq5.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq6.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq9.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq10.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq11.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq12.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq13.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq15.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq16.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq17.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq20.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq21.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq22.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq25.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
eq_cases_on.lean fix(library/compiler/preprocess): expand eq.cases_on 2017-02-07 21:19:01 -08:00
eqn_issue.lean fix(library/equations_compiler/structural_rec): bug in decoder 2016-12-18 22:51:02 -08:00
equation_with_values.lean feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08:00
eval_constant.lean feat(library/tactic/eval): eval_expr for arbitrary expressions 2016-10-03 19:01:22 -07:00
eval_expr_bug.lean fix(library/vm/vm): bug at get_constant 2016-10-04 01:58:39 -07:00
even_perf.lean perf(library/compiler): add common subexpression elimination 2016-12-11 14:43:51 -08:00
ex.lean
exact_perf.lean fix(library/type_context): failure cache 2016-12-13 07:50:03 -08:00
exact_tac1.lean
example1.lean
exfalso1.lean
exists_intro1.lean feat(frontends/lean/token_table): add ASCII notation for anonymous constructor 2016-09-25 13:48:52 -07:00
export.lean
export2.lean
fib_wrec.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
find.lean feat(library/init/meta/tactic): add dec_trivial notation 2016-11-23 11:42:57 -08:00
fingerprint.lean chore(tests/lean/run): fix tests 2016-10-03 21:44:48 -07:00
format.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
full.lean
fun.lean
fun_info1.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
gcd.lean chore(library/init): cleanup proofs using new elaborator 2016-09-23 17:36:32 -07:00
generalize_inst.lean fix(library/tactic/generalize_tactic): instantiate mvars before calling kabstract 2017-02-01 18:48:10 -08:00
generalizes.lean
have1.lean
have2.lean
have3.lean
have4.lean
have6.lean
heap.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
help_cmd.lean
hinst_lemma1.lean feat(library/tactic/congruence/hinst_lemma): add heuristic instantiation lemmas 2016-12-25 20:11:58 -08:00
hinst_lemmas1.lean feat(library/init/meta/smt/ematch): add hinst_lemmas API 2017-01-04 18:04:53 -08:00
ho.lean
id.lean
if_dollar_prec.lean fix(frontends/lean/builtin_exprs): ite/dite prec should be lowest 2017-01-26 18:52:20 +01:00
imp.lean
imp2.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
imp3.lean
implicit.lean
ind0.lean
ind1.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
ind2.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
ind3.lean
ind5.lean
ind6.lean
ind7.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
ind8.lean
ind_bug.lean
ind_cnst_params.lean feat(frontends/lean): allow constructor parameters to be declared before ':' 2017-01-31 15:11:39 -08:00
ind_ns.lean
ind_tac1.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
indbug2.lean
indimp.lean
induction_on.lean
induction_on_aux_rec_bug.lean fix(library/constructions/induction_on): induction_on was not being marked as aux_recursor 2016-12-20 22:41:50 -08:00
induction_tac3.lean
induction_tactic_delta.lean
inductive_nonrec_after_rec.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
injection1.lean
inliner_bug.lean fix(library/compiler): move inliner to the beginning 2016-11-08 16:14:01 -08:00
inst_bug.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
int_eq_num.lean feat(library/equations_compiler): int constants 2016-12-25 10:00:18 -08:00
interactive1.lean feat(library/tactic/simplify): use propext in rewriting rules when simplify_config.use_axioms is tt 2016-10-19 17:59:01 -07:00
interp.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
intros_defeq_canonizer_bug.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
IO1.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
IO2.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
IO3.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
IO4.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
is_def_eq_perf_bug.lean
is_true.lean
isabelle.lean feat(library/data): add lazy_list 2017-02-08 12:01:46 -08:00
itac.lean feat(frontends/lean/tactic_notation): nested interactive tactics 2016-09-30 14:53:07 -07:00
K_new_elab.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
kcomp.lean
kha_inst_bug.lean test(tests/lean/run): add regression test 2016-12-17 14:08:10 -08:00
lambda_simp.lean feat(library/tactic/simplify): add basic support for lambda-expressions 2016-10-19 14:15:56 -07:00
let1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
let2.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
let3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
let_vm_bug.lean fix(library/compiler/erase_irrelevant): bug at is_comp_irrelevant 2016-10-27 11:51:37 +08:00
level_bug1.lean
level_bug2.lean
level_bug3.lean
lift.lean
lift2.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
lift_nested_rec.lean feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08:00
list_notation.lean refactor(library/init): reorganize files and cleanup notation 2016-09-25 13:37:45 -07:00
listex.lean test(tests/lean/run): add tactic examples 2017-01-06 18:48:03 -08:00
listex2.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
listex3.lean chore(tests/lean/run/listex3): we don't need the unit trick anymore 2017-02-04 13:55:51 -08:00
listex4.lean fix(library/tactic/backward/backward_chaining): bug in back_chaining tactic 2017-01-07 11:19:03 -08:00
local_notation.lean
match2.lean feat(frontends/lean): change subtype notation (again) 2016-09-21 17:02:18 -07:00
match3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
match4.lean
match_anonymous_constructor.lean feat(frontends/lean/token_table): add ASCII notation for anonymous constructor 2016-09-25 13:48:52 -07:00
match_convoy.lean chore(library/init): adjust Sort vs Type in definitions 2017-01-30 12:50:18 -08:00
match_convoy2.lean refactor(library/init/bool): put main operations in the top-level 2016-09-25 13:32:15 -07:00
match_convoy3.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
match_expr.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
match_expr2.lean
match_fun.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
match_pattern1.lean refactor(library): rename pr1/pr2 ==> fst/snd 2016-09-21 09:48:39 -07:00
match_pattern2.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
matrix.lean
matrix2.lean
max_memory.lean
mem_nil.lean refactor(library/init/core): simpler has_insert type class with out_param 2017-01-30 18:50:21 -08:00
meta1.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
meta2.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
meta3.lean
meta_env1.lean feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class 2016-09-29 17:56:35 -07:00
meta_expr1.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
meta_level1.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
meta_tac1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
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 fix(library/type_context): allow assigned regular meta-variables to be "read" in tmp-mode 2016-10-21 13:33:07 -07:00
mk_byte.lean feat(library/simplify): use custom matcher in the simplifier, and remove hack from type_context 2017-02-08 22:24:13 -08:00
mk_dec_eq1.lean
mk_dec_eq_instance_indices.lean fix(meta/mk_dec_eq_instance): handle indices and ginductives 2016-10-13 10:12:37 -07:00
mk_dec_eq_instance_nested.lean fix(meta/mk_dec_eq_instance): handle indices and ginductives 2016-10-13 10:12:37 -07:00
mk_inhabited1.lean
mk_instance1.lean
monad_univ_lift.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
mutual_inductive.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
my_tac_class.lean fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
n3.lean
n5.lean
name_resolution_at_tactic_execution_time.lean fix(frontends/lean): name resolution at tactic execution time 2016-11-24 10:55:39 -08:00
name_resolution_with_params_bug.lean fix(library/init/meta/interactive): name resolution problems in parametric sections 2017-02-03 14:04:59 -08:00
namespace_local.lean
nat_bug.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
nat_bug2.lean
nat_bug4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
nat_bug7.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
nat_sub_ematch.lean fix(library/init/data/nat/lemmas): avoid bad patterns in nat sub ematch lemmas 2017-01-22 19:48:01 -08:00
nateq.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
nested_begin_end.lean
nested_common_subexpr_issue.lean chore(tests/lean/run/nested_common_subexpr_issue): typo 2017-01-09 15:36:49 -08:00
nested_inductive.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
new_elab1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
new_elab2.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
no_confusion1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
no_confusion_bug.lean
noncomputable_example.lean chore(tests/lean): fix tests 2017-01-30 11:54:00 -08:00
noncomputable_meta.lean fix(frontends/lean/decl_cmds): allow noncomputable meta 2016-10-08 22:21:56 -07:00
norm_num_tst.lean test(tests/lean/run/norm_num_tst): add norm_num tactic tests 2016-12-17 21:19:15 -08:00
not_bug1.lean
ns.lean
ns1.lean
ns2.lean
num.lean
num_sub.lean
occurs_check_bug1.lean chore(library/init): use 'instance' 2016-09-23 14:00:34 -07:00
offset1.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
one.lean
one2.lean
opaque_hint_bug.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
opt1.lean
opt_param_cc.lean refactor(library/init/meta/fun_info): cleanup fun_info API 2017-01-31 18:01:54 -08:00
opt_param_cnsts.lean feat(frontends/lean): allow default parameter values in constant decls 2017-01-31 15:19:47 -08:00
over2.lean
over3.lean feat(frontends/lean/elaborator): improve overloading support 2016-09-28 20:54:11 -07:00
over_subst.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
overload_issue.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
pack_unpack1.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
pack_unpack2.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
pack_unpack3.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
parent_struct_inst.lean feat(frontends/lean/token_table): add ASCII notation for anonymous constructor 2016-09-25 13:48:52 -07:00
parent_struct_ref.lean
partial_explicit.lean
partial_explicit1.lean
period_after_eqns.lean fix(frontends/lean/definition_cmds): allow '.' after equations 2017-01-22 12:51:23 -08:00
pp_unit.lean
prec_max.lean
pred_to_subtype_coercion.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
pred_using_structure_cmd.lean
premises.lean
print_inductive.lean
print_poly.lean
priority_test.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
priority_test2.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
private_names.lean feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword 2016-09-24 18:40:57 -07:00
prod_notation.lean
protected.lean
ptst.lean
qed_perf_bug.lean
qexpr1.lean
quote1.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
rb_map1.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
rec_and_tac_issue.lean fix(library/type_context): issue #1258 again 2016-12-22 10:51:16 -08:00
rec_eq_ematch_bug.lean fix(library/tactic/smt/smt_state): remove auxiliary hypotheses added by the equation compiler 2017-01-08 10:36:38 -08:00
rec_meta_issue.lean test(tests/lean/run): add test for meta recursive definition wo recursive equation 2017-02-04 13:53:12 -08:00
record1.lean
record2.lean
record4.lean
record7.lean
record8.lean
record9.lean feat(frontends/lean): (Type u) can't be a proposition 2017-01-30 11:54:00 -08:00
record10.lean feat(library/init): add basic algebra 2016-09-30 20:51:22 -07:00
reflexive_elim_prop_bug.lean fix(library/equations_compiler/structural_rec): missing case: reflexive inductive type eliminating into Prop 2016-11-23 13:56:01 -08:00
regset.lean refactor(library/init/core): simpler has_mem type class with out_param 2017-01-30 18:43:05 -08:00
rel_tac1.lean
reserve.lean
resolve_name_bug.lean fix(library/init/meta/interactive): resolve name at interactive unfold tactics 2016-11-18 16:14:03 -08:00
revert_crash.lean fix(library/type_context): bug in revert method 2017-02-01 10:51:24 -08:00
root.lean
run_tactic1.lean chore(tests/lean/run): fix tests 2016-10-03 21:44:48 -07:00
rvec.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
rw_set1.lean chore(tests/lean/run): adjust tests 2016-11-21 12:23:36 -08:00
rw_set3.lean refactor(library/tactic/simp_lemmas): new caching mechanism 2016-10-06 20:20:01 -07:00
rw_set4.lean feat(library/tactic/simplify): use propext in rewriting rules when simplify_config.use_axioms is tt 2016-10-19 17:59:01 -07:00
sec_bug.lean
sec_notation.lean
sec_var.lean
seclvl.lean
secnot.lean
section1.lean
section2.lean
section3.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
section4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
section5.lean
section_var_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
set1.lean chore(library/init): minor changes 2016-09-27 07:23:51 -07:00
set_attr1.lean chore(tests/lean): fix tests 2016-11-05 11:51:29 -07:00
shadow1.lean
sigma_match.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
simp1.lean refactor(library/tactic/simplify): delete old simplifier 2016-10-19 14:03:14 -07:00
simp_attr_eqns.lean feat(library/tactic/simp_lemmas): convenient way of adding equational lemmas of a definition to a simp set 2017-01-14 22:16:16 -08:00
simp_eqns.lean feat(library/init/meta/interactive): add get_eqn_lemmas_for tactic, allow user to provide definition name as an argument to simp 2017-01-06 11:45:09 -08:00
simp_if_true_false.lean fix(library/init/logic.lean): if_true and if_false take instance as implicit instead of inst_implicit 2016-11-21 12:27:40 -08:00
simp_lemma_issue.lean fix(library/init/meta/smt/ematch,library/tactic/simp_lemmas): trick for adding equations of a definition to a simp/hinst lemma set 2017-01-18 02:05:04 -08:00
simp_partial_app.lean feat(library/type_context): improve offset trick in the unifier 2017-02-04 17:15:05 -08:00
simp_proof_failure.lean feat(library/app_builder): use Semireducible if caller did not specify a transparency_mode and ctx.mode() is Reducible or None 2016-12-23 14:41:22 -08:00
simp_univ_metavars.lean fix(library/tactic/simplify): relax test 2017-01-23 09:59:06 -08:00
simple.lean fix(frontends/lean/elaborator): use expected type when elaborating application for the form (c^.fn a) 2017-02-02 19:56:50 -08:00
simplifier_custom_relations.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
simplify_with_hypotheses.lean feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -08:00
size_of1.lean feat(library/init/meta/tactic): add dec_trivial notation 2016-11-23 11:42:57 -08:00
sizeof2.lean
smt_array.lean test(tests/lean/run): add "array" test 2017-01-24 22:00:33 -08:00
smt_assert_define.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
smt_destruct.lean refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
smt_ematch1.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
smt_ematch2.lean refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
smt_ematch3.lean refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
smt_ematch_alg_issue.lean refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
smt_facts_as_hinst_lemmas.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
smt_not_exists.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
smt_tests.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
smt_tests2.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
smt_tests3.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
sorry.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
stateT1.lean chore(*): don't use upper case letter for type variables, and camelCase for declarations 2016-11-17 14:54:08 -08:00
struc_names.lean
struct_bug1.lean
struct_inst_exprs2.lean
struct_value.lean chore(library/init): adjust Sort vs Type in definitions 2017-01-30 12:50:18 -08:00
structure_doc_string.lean fix(frontends/lean/parser): structure followed by doc string 2017-01-23 10:35:07 -08:00
structure_result_universe.lean fix(frontends/lean/structure_cmd): handle is_one_placeholder 2016-10-02 08:07:19 -07:00
structure_test.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
sub.lean feat(frontends/lean): change subtype notation (again) 2016-09-21 17:02:18 -07:00
sub_bug.lean feat(frontends/lean): change subtype notation (again) 2016-09-21 17:02:18 -07:00
subst_tac1.lean
suffices.lean
sufficies.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
super.lean
super_examples.lean chore(tests/lean/run/super_examples): clean up 2017-01-10 09:07:37 -08:00
super_tests.lean fix(test/lean/run/super_tests): fix try_sup API change 2017-01-13 11:33:35 -08:00
t1.lean
t2.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
t3.lean
t4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
t5.lean
t6.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
t7.lean
t9.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
t10.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
t11.lean chore(frontends/lean): remove dead code from parser 2016-09-19 17:04:59 -07:00
tactic_mode_scope_bug.lean fix(frontends/lean/parser): scope in tactic mode 2016-12-10 09:39:13 -08:00
tc_inout1.lean feat(library/type_context, frontends/lean/elaborator): type classes with output parameters 2017-01-30 18:32:54 -08:00
tc_loop.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
test_perm_ac1.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
test_single.sh refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
thunk_overload.lean feat(frontends/lean, library/init): add 'thunk' gadget 2017-01-31 18:41:59 -08:00
tick_id.lean feat(frontends/lean/scanner): allow ' in the beginning of identifiers 2016-11-17 11:53:21 -08:00
trace_call_stack_segfault.lean fix(library/vm/vm): fix segfault in call_stack_fn 2017-01-17 16:00:01 -08:00
trace_tst.lean feat(frontends/lean, library/init): add 'thunk' gadget 2017-01-31 18:41:59 -08:00
tuple_head_issue.lean chore(library/data): rename tuple => vector 2017-01-26 22:11:10 -08:00
type_equations.lean
u_eq_max_u_v.lean feat(library/type_context): do not fail on universe constraints of the form ?u =?= max ?u v 2017-02-02 22:30:30 -08: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_issue.lean chore(tests/lean/run): fix tests 2017-01-17 15:50:54 -08:00
uni_issue1.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
uni_var_bug.lean
unicode.lean
unification_hints.lean refactor(library/init): move unification_hint structure to init folder 2016-09-28 09:35:19 -07:00
unify_fo_approx_bug1.lean
univ1.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
univ2.lean
univ_bug1.lean
univ_bug2.lean
univ_cnstr1.lean fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type 2017-01-30 11:54:00 -08:00
univ_delay_thm_bug.lean fix(frontends/lean/definition_cmds): implicit universe theorem parameters bug 2016-11-29 11:12:43 -08:00
univ_elab_issue.lean fix(frontends/lean/elaborator): universe elaboration issue 2017-01-10 22:35:12 -08:00
unreachable_cases.lean feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
untrusted_examples.lean fix(frontends/lean): type check examples 2016-09-27 14:39:55 -07:00
user_simp_attributes.lean feat(library/init/meta,library/tactic/simplifier): user defined simp attributes 2016-10-03 21:39:17 -07:00
using_smt1.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
using_smt2.lean chore(tests/lean/run): repair SMT tests 2017-01-13 13:36:19 -08:00
using_smt3.lean fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages 2017-02-07 20:25:28 -08:00
vars_anywhere.lean
vector2.lean
vector3.lean
vm_eval1.lean
wfrec1.lean
whenIO.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
whnfinst.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
with_update_class.lean fix(frontends/lean/elaborator): structure instance update with type classes 2016-10-02 11:36:22 -07:00
xrewrite1.lean feat(library/tactic): add "approximate" parameter to apply_core and rewrite_core 2016-12-10 10:24:05 -08:00