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 0ba60e62d7 feat(kernel/quotient/quotient): make quotient module robust against users that define their own prelude's 
Before this commit, an user could define their own prelude and change
the types of quot, quot.mk, quot.lift or quot.ind.
By doing that, they could prove false.

This commit prevents this kind of abuse.
It also modifies the definition of `quot` and avoids the `setoid`
dependency.
The previous `quot` type is now called `quotient`, and it is defined
using the new `quot` type provided by the kernel.

See discussion at #1330
2017-01-24 15:59:38 -08:00
..
252.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
331.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
444.lean
445.lean
490.lean feat(frontends/lean): use new notation for declaring universes in constant and structure decls 2016-09-13 21:45:16 -07:00
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 feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
774.lean
791.lean
808.lean refactor(library/normalize): remove unfold and unfold_full attributes 2016-09-05 08:40:58 -07:00
817.lean
967.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
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 fix(library/equations_compiler/elim_match): bug at complete transition 2016-10-19 09:10:19 -07: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 fix(library/equations_compiler/elim_match): see #1216 2016-12-08 15:38:14 -08:00
1218.lean test(tests/lean/run): add test for @1218 2016-12-08 14:10:47 -08:00
1226.lean feat(library/type_context): add support for offset constraints in the unifier 2016-12-06 16:51: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
ac_refl1.lean test(tests/lean/run): add ac_refl tests 2016-12-29 19:51:18 -08:00
ack.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
anonymous_param.lean feat(frontends/lean/parser): add support for anonymous parameters 2016-12-10 11:07:58 -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 feat(frontends/lean): quoted names 2016-07-22 19:06:57 -07:00
apply2.lean feat(frontends/lean): quoted names 2016-07-22 19:06:57 -07:00
apply3.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
apply4.lean feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -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(tests/lean/run): adjust tests 2016-11-21 12:23:36 -08:00
at_at_bug.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
atomic2.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
atomic_notation.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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(library/vm/vm): invoke debugger (aka vm_monitor) 2016-11-14 14:45:49 -08:00
basic_monitor1.lean feat(library/vm,library/tactic/vm_monitor): use optionT to define vm monad 2016-11-14 16:13:56 -08:00
basic_monitor2.lean feat(library/tactic/vm_monitor): add vm_decl introspection 2016-11-14 18:04:53 -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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
bor_lazy.lean
bug5.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
bug6.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07: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 feat(frontends/lean, library): remove attribute and metaclass scoping 2016-07-29 23:44:21 -04:00
calc_bug.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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 feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
cases_bug2.lean fix(library/user_recursors): add support for automatically generated recursors 2016-08-21 17:17:48 -07:00
cases_bug3.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
cases_crash1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
cases_tac1.lean chore(tests/lean/run): fix tests 2017-01-17 15:50:54 -08:00
cast_sorry_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
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 fix(library/tactic/congruence/congruence_closure): missing proof construction step 2016-12-24 08:43: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 refactor(library/tools/super): move examples to test folder 2016-12-16 19:05:32 -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 feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
cody2.lean chore(tests/lean/run): make sure tests work with new elaborator 2016-09-18 14:48:47 -07:00
coe_univ_bug.lean fix(frontends/lean): use coercions to sort at elaborate_type 2016-09-26 16:47:31 -07: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 fix(library/compiler/elim_recursors): bug in elim_recursors 2016-11-02 14:19:28 -07:00
confuse_ind.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07: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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
consume.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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
default_field_values1.lean feat(frontends/lean): add default field values 2017-01-22 21:25:49 -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
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 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
e5.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
e15.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
e16.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
elab3.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
elab4.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab5.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab6.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab_bool.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
elab_crash1.lean feat(frontends/lean/parser): keep list of tasks that have to succeed 2017-01-17 15:31:17 -08: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
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
enum.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
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
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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
exact_perf.lean fix(library/type_context): failure cache 2016-12-13 07:50:03 -08:00
exact_tac1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
example1.lean chore(tests/lean/run): make sure tests work with new elaborator 2016-09-18 14:48:47 -07:00
exfalso1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
exists_intro1.lean feat(frontends/lean/token_table): add ASCII notation for anonymous constructor 2016-09-25 13:48:52 -07:00
export.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
fun.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
fun_info1.lean feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
gcd.lean chore(library/init): cleanup proofs using new elaborator 2016-09-23 17:36:32 -07:00
generalizes.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
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 feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
id.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
imp.lean feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
imp2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
imp3.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
implicit.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
ind0.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
ind1.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
ind2.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
ind3.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
ind5.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
ind6.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
ind7.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
ind8.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
ind_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
ind_ns.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
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 feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
indimp.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
induction_on.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
induction_tactic_delta.lean feat(src/library/inductive_compiler): support for nested inductive types 2016-09-16 12:50:59 -07:00
inductive_nonrec_after_rec.lean test(tests/lean/run): test inductive datatypes with non-recursive arguments after recursive ones 2017-01-16 22:59:17 -08:00
injection1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
inliner_bug.lean fix(library/compiler): move inliner to the beginning 2016-11-08 16:14:01 -08:00
inst_bug.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07: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 chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -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 feat(library/type_context): mimic behavior of the kernel type_checker 2016-09-03 16:43:33 -07:00
is_true.lean refactor(library/init/logic): rename decidable.tt/ff to decidable.is_true/is_false 2016-09-13 13:40:02 -07: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 feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
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 feat(frontends/lean/decl_util): use the same notation for declaring universes in mutual and single decls 2016-09-13 21:05:18 -07:00
lift2.lean feat(frontends/lean/decl_util): use the same notation for declaring universes in mutual and single decls 2016-09-13 21:05:18 -07: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 fix(library/tactic/backward/backward_chaining): bug in back_chaining tactic 2017-01-07 11:19:03 -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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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 feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
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 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_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 feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
match_expr2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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 feat(frontends/lean): use new notation for declaring universes in constant and structure decls 2016-09-13 21:45:16 -07:00
matrix2.lean feat(frontends/lean): use new notation for declaring universes in constant and structure decls 2016-09-13 21:45:16 -07:00
max_memory.lean
mem_nil.lean feat(library/type_context): add yet another approximation to unifier 2016-12-19 20:34:07 -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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
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 chore(frontends/lean/pp, library/pp_options): pp.lazy_abstraction ==> pp.delayed_abstraction 2016-08-03 18:45:47 -07:00
meta_tac3.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
meta_tac4.lean chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -07:00
meta_tac5.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
meta_tac6.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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_dec_eq1.lean chore(tests/lean): providing universes 2016-09-17 12:54:20 -07:00
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 feat(library/init/meta): add mk_inhabited_instance tactic 2016-07-20 21:01:50 -04:00
mk_instance1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
monad_univ_lift.lean feat(library/type_context): universe constraint postponement 2016-09-28 15:30:14 -07: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 refactor(frontends/lean): interactive tactic support 2017-01-21 22:38:47 -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
namespace_local.lean
nat_bug.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
nat_bug2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
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(meta/mk_dec_eq_instance): handle indices and ginductives 2016-10-13 10:12:37 -07: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 feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
noncomputable_example.lean fix(frontends/lean): type check examples 2016-09-27 14:39:55 -07: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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
ns.lean chore(tests/lean/run): preparing tests for new elaborator 2016-07-31 17:45:43 -07:00
ns1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
ns2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
num.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
num_sub.lean
occurs_check_bug1.lean chore(library/init): use 'instance' 2016-09-23 14:00:34 -07:00
offset1.lean feat(library/type_context): move offset constraint resolution to lazy delta loop 2016-12-08 11:00:15 -08:00
one.lean feat(frontends/lean/decl_util): use the same notation for declaring universes in mutual and single decls 2016-09-13 21:05:18 -07:00
one2.lean feat(frontends/lean/decl_util): use the same notation for declaring universes in mutual and single decls 2016-09-13 21:05:18 -07:00
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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
over2.lean chore(tests/lean/run): make sure tests work with new elaborator 2016-09-18 14:48:47 -07:00
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 feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08:00
pack_unpack2.lean feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08:00
pack_unpack3.lean feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names 2017-01-06 11:40:34 -08: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 feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
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 fix(frontends/lean): use coercions to sort at elaborate_type 2016-09-26 16:47:31 -07:00
pred_using_structure_cmd.lean
premises.lean
print_inductive.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
print_poly.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
protected.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
ptst.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
qed_perf_bug.lean perf(kernel/type_checker): use definitional height again at is_def_eq 2016-09-03 16:18:39 -07:00
qexpr1.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
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
record1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
record2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
record4.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
record7.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
record8.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
record9.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07: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
rel_tac1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
reserve.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
resolve_name_bug.lean fix(library/init/meta/interactive): resolve name at interactive unfold tactics 2016-11-18 16:14:03 -08:00
root.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
run_tactic1.lean chore(tests/lean/run): fix tests 2016-10-03 21:44:48 -07:00
rvec.lean test(tests/lean/run): test inductive datatypes with non-recursive arguments after recursive ones 2017-01-16 22:59:17 -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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
sec_notation.lean
sec_var.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
seclvl.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
secnot.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
section1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
section2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
section3.lean feat(library/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07:00
section4.lean chore(frontends/lean): remove 'new_elaborator' option 2016-09-20 08:32:37 -07:00
section5.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
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 feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -07:00
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 fix(library/tactic/simplify): make sure a partially applied lhs can be used to rewrite terms with "more arguments" in simp 2017-01-23 19:53:49 -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 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
simplifier_custom_relations.lean refactor(library/init/meta/simp_tactic): use default field values at simplify_config 2017-01-23 10:22:48 -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 feat(library/init/datatypes): add default has_sizeof instance 2016-09-02 10:32:37 -07: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/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07: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 feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
struct_bug1.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
struct_inst_exprs2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
struct_value.lean feat(frontends/lean/token_table): add ASCII notation for anonymous constructor 2016-09-25 13:48:52 -07: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 refactor(library): rename pr1/pr2 ==> fst/snd 2016-09-21 09:48:39 -07: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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
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): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07: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
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_loop.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07: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
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
tuple_head_issue.lean fix(library/init/meta/contradiction_tactic): make sure contradiction uses whnf for constructor-eq-constructor case 2017-01-20 18:42:27 -08:00
type_equations.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07: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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
unicode.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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 feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
univ1.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
univ2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
univ_bug1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
univ_bug2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
univ_cnstr1.lean feat(library/type_context): universe constraint postponement 2016-09-28 15:30:14 -07: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/noncomputable): improve is_noncomputable 2016-09-08 14:02:23 -07: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 refactor(library/init/meta/smt): use default value for config structures 2017-01-23 14:18:06 -08:00
vars_anywhere.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
vector2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
vector3.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
vm_eval1.lean feat(frontends/lean): Type is now (Type 1) 2016-09-17 14:30:54 -07:00
wfrec1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
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