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 13f0d4e09a refactor(library/equations_compiler): new equation lemma generation 
The idea is to generate a lemma based on the left-hand-side provided by
the user. This feature is essential for supporting the derived inductive
datatype constructors.
2016-09-02 14:04:09 -07: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
600a.lean
600b.lean
600c.lean
662.lean feat(frontends/lean/parser): _ is an anonymous variable again in patterns. 2016-08-23 14:06:24 -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 chore(library, tests): use new attribute chaining syntax 2016-08-16 13:49:03 -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/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
1093.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
ack.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
all_goals1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
app_builder_tac1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
arity1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
as.lean
assert_tac1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
assert_tac3.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
assoc_flat.lean feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
atomic2.lean
atomic_notation.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
back_chaining1.lean feat(library/tactic/backward): finish backward chaining tactic 2016-07-10 13:49:28 -07:00
back_chaining2.lean feat(library/tactic/backward): finish backward chaining tactic 2016-07-10 13:49:28 -07:00
back_chaining3.lean feat(library/tactic/backward/backward_chaining): add 'pre_tactic' to backward_chaining_core 2016-07-10 16:11:13 -07:00
back_chaining4.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
basic.lean
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 feat(library/init/bool): mark bor, band and cond as inline 2016-06-05 13:03:33 -07:00
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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
calc_imp.lean
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_crash1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
cases_tac1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
cast_sorry_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
choice_ctx.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
class1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
class2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
class3.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
class6.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
class11.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
class_bug1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
class_bug2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
cody1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
cody2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
comment.lean
confuse_ind.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
congr_imp_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
congr_lemma1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
const_choice.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -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 feat(library/init/meta/contradiction_tactic): improve contradiction tactic 2016-06-16 18:32:08 -07:00
contra2.lean feat(library/init/meta/contradiction_tactic): improve contradiction tactic 2016-06-16 18:32:08 -07:00
contra3.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
cute_binders.lean feat(frontends/lean/parser): cute binders 2016-07-08 07:50:58 -07:00
dec_trivial_loop.lean refactor(library): remove unifier_plugin 2016-03-21 17:57:53 -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
def1.lean feat(frontends/lean/definition_cmds): basic xdefinition_cmd_core 2016-08-13 15:08:32 -07:00
def2.lean feat(frontends/lean/definition_cmds): basic xdefinition_cmd_core 2016-08-13 15:08:32 -07:00
def3.lean feat(frontends/lean/definition_cmds): invoke compiler 2016-08-13 16:45:32 -07:00
def4.lean fix(frontends/lean/definition_cmds): collect implicit args in the type 2016-08-13 16:54:17 -07:00
def5.lean fix(frontends/lean/definition_cmds): parameter handling 2016-08-23 21:13:54 -07:00
def6.lean refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic): 2016-08-28 13:15:10 -07:00
def7.lean refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic): 2016-08-28 13:15:10 -07:00
def8.lean refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic): 2016-08-28 13:15:10 -07:00
def9.lean refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic): 2016-08-28 13:15:10 -07:00
def10.lean refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic): 2016-08-28 13:15:10 -07:00
def11.lean refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic): 2016-08-28 13:15:10 -07:00
def13.lean test(tests/lean/run/def13): add map-like test for dependent patter matching 2016-08-28 14:45:39 -07:00
def_brec1.lean feat(library/equations_compiler/structural_rec): generate brec_on-based function 2016-08-29 15:58:13 -07:00
def_brec2.lean refactor(library/equations_compiler): new equation lemma generation 2016-09-02 14:04:09 -07:00
def_brec3.lean fix(frontends/lean/pp): remove unnecessary parenthesis when pretty printing (A -> (Pi (b : B), C b)) 2016-08-29 16:36:04 -07:00
def_brec4.lean feat(library/type_context): improve on_is_def_eq_failure for stuck terms 2016-08-30 10:51:40 -07:00
def_brec_reflexive.lean fix(library/equations_compiler/structural_rec): support for reflexive inductive datatypes 2016-08-31 10:46:32 -07:00
def_complete_bug.lean refactor(library/equations_compiler): new equation lemma generation 2016-09-02 14:04:09 -07:00
div_wf.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
do_match_else.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
dsimp_at1.lean chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -07:00
e1.lean
e2.lean
e3.lean
e4.lean
e5.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
e15.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
e16.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
elab3.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -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_bug1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
elab_crash1.lean refactor(library/init/meta): qexpr ==> pexpr 2016-08-05 17:04:36 -07:00
elab_failure.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
empty_eq.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
empty_match.lean chore(tests/lean/run): preparing tests for new elaborator 2016-07-31 17:45:43 -07:00
empty_match_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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 feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
eq2.lean feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
eq4.lean
eq5.lean
eq6.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
eq9.lean feat(frontends/lean/parser): simplify pattern semantics '_' in a pattern is always a anonymous variable 2016-08-13 22:14:40 -07:00
eq10.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
eq11.lean feat(frontends/lean/parser): _ is an anonymous variable again in patterns. 2016-08-23 14:06:24 -07:00
eq12.lean feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
eq13.lean feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
eq15.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
eq16.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
eq17.lean feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -07:00
eq20.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
eq21.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
eq22.lean feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
eq25.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07: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_tac1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
example1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
exfalso1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -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(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
fibrant_class1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
fibrant_class2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
find.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
fingerprint.lean feat(library/attribute_manager): fingerprints 2016-08-23 08:20:37 -07:00
format.lean refactor(library): move 'meta' to 'init' folder 2016-06-06 19:08:07 -07: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 chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
gcd.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
generalizes.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
group.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
group3.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
have1.lean feat(frontends/lean): remove difference between 'have' and 'assert' 2016-02-29 11:28:20 -08:00
have2.lean feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking 2016-02-29 12:31:23 -08:00
have3.lean
have4.lean
have6.lean chore(frontends/lean): remove 'assert' keyword 2016-06-17 14:20:26 -07:00
help_cmd.lean
ho.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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
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
impbug1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
impbug2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
impbug3.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
impbug4.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/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
ind2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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
indbug2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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_tac3.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
induniv.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
injection1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
inst_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
interp.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
IO1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
IO2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
IO3.lean chore(tests/lean): disable tests 2016-06-10 18:29:41 -07:00
IO4.lean test(tests/lean/run): add IO test 2016-05-25 16:04:54 -07:00
is_true.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
kcomp.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
let1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
let2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
level_bug1.lean
level_bug2.lean
level_bug3.lean
lift.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
lift2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
list_elab1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07: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 chore(tests/lean/run/match2): missing test 2016-08-21 15:55:56 -07:00
match3.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
match4.lean feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
match_convoy.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
match_expr.lean feat(library/init/meta/match_tactic): add helper tactics on top of match tactic 2016-08-06 14:13:41 -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
match_pattern1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
match_pattern2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
matrix.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
matrix2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
max_memory.lean
meta1.lean feat(frontends/lean): add meta_definition and meta_constant commands 2016-06-01 09:12:41 -07:00
meta2.lean feat(frontends/lean): allow unbounded recursion in meta_definitions 2016-06-01 09:55:07 -07:00
meta3.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
meta_env1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
meta_expr1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
meta_level1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
meta_tac1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -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 feat(frontends/lean/old_elaborator): interface old_elaborator with new tactic framework 2016-06-13 13:59:01 -07:00
mk_dec_eq1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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
n3.lean
n5.lean
namespace_local.lean
nat_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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 feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
nat_bug7.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
nateq.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
nested_begin_end.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -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
not_bug1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
notation_priority.lean
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(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
one.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
one2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
opaque_hint_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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 only use init and system.IO 2016-08-11 18:13:00 -07:00
over_subst.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
parent_struct_inst.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
parent_struct_ref.lean
partial_explicit.lean feat(frontends/lean/builtin_exprs): simplify '@' and '@@' 2016-07-02 11:08:18 +01:00
partial_explicit1.lean feat(frontends/lean/builtin_exprs): simplify '@' and '@@' 2016-07-02 11:08:18 +01:00
pattern2.lean chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -07:00
pattern3.lean chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -07:00
pp_unit.lean feat(frontends/lean/pp): pp unit.star 2016-06-08 17:30:11 -07:00
pquot.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
prec_max.lean refactor(frontends/lean): disable '!' operator, and adjust standard library 2016-07-02 01:41:46 +01:00
pred_using_structure_cmd.lean feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command 2016-02-22 16:09:44 -08:00
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_no_pattern.lean
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/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
priority_test2.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
private_names.lean chore(library, tests): use new attribute chaining syntax 2016-08-16 13:49:03 -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
qexpr1.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
quote1.lean refactor(library/init/meta): qexpr ==> pexpr 2016-08-05 17:04:36 -07:00
rb_map1.lean refactor(library): move 'meta' to 'init' folder 2016-06-06 19:08:07 -07: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 chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
record10.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07: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
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(frontends/lean): run_tactic ==> run_command 2016-08-18 12:53:21 -07:00
rw_set1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
rw_set3.lean refactor(simplifier): many fixes, extensions, and tests 2016-08-19 14:57:03 -07:00
rw_set4.lean chore(library, tests): use new attribute chaining syntax 2016-08-16 13:49:03 -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
section4.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
section5.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
set.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
set2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
set_attr1.lean feat(library/tactic/user_attribute): add set_basic_attribute and unset_attribute tactics 2016-09-01 14:17:05 -07:00
shadow1.lean feat(frontends/lean): new pattern matching validation 2016-08-07 11:31:11 -07:00
show2.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
sigma_match.lean feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
simp1.lean chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -07:00
simp_ext1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
simp_ext_refl.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
simp_orderings.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
simp_prove_fn.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
simple.lean
simplifier_assoc.lean refactor(simplifier): many fixes, extensions, and tests 2016-08-19 14:57:03 -07:00
simplifier_canonize_instances.lean refactor(simplifier): many fixes, extensions, and tests 2016-08-19 14:57:03 -07:00
simplifier_canonize_subsingletons.lean refactor(simplifier): many fixes, extensions, and tests 2016-08-19 14:57:03 -07:00
simplifier_custom_relations.lean refactor(simplifier): many fixes, extensions, and tests 2016-08-19 14:57:03 -07:00
simplifier_prop.lean refactor(simplifier): many fixes, extensions, and tests 2016-08-19 14:57:03 -07:00
simplifier_synth_congr.lean refactor(simplifier): many fixes, extensions, and tests 2016-08-19 14:57:03 -07:00
simplifier_topdown.lean refactor(simplifier): many fixes, extensions, and tests 2016-08-19 14:57:03 -07:00
simplify_with_hypotheses.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
size_of1.lean refactor(init/datatypes, init/logic): define sizeof instances and simp lemmas 2016-09-01 10:33:50 -07:00
sizeof2.lean feat(library/init/datatypes): add default has_sizeof instance 2016-09-02 10:32:37 -07:00
sorry.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
st_options.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
stateT1.lean chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -07: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
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
structure_test.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
sub.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
sub_bug.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
subst_tac1.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
suffices.lean
sum_bug.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
super.lean
t1.lean
t2.lean
t3.lean
t4.lean
t5.lean
t6.lean
t7.lean
t9.lean
t10.lean
t11.lean
tc_loop.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
test_perm_ac1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00
test_single.sh
trace_tst.lean feat(library/vm): add 'trace' 2016-06-08 16:32:20 -07:00
trans.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07: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(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07:00
uni_issue1.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -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 chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -07:00
unify_fo_approx_bug1.lean feat(frontends/lean): remove #elab command 2016-08-02 15:05:24 -07:00
univ1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -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
unreachable_cases.lean feat(frontends/lean): revising inaccessible terms syntax again :( 2016-08-19 13:57:12 -07:00
untrusted_examples.lean chore(frontends/lean): coercions are disabled by default 2016-07-29 13:03:23 -07:00
uuu.lean feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd 2016-08-17 07:34:03 -07: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 chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -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 refactor(library): move 'none', 'some', 'tt', 'ff' to top-level 2016-06-25 12:39:19 -07:00
whnfinst.lean chore(library, tests): switch to new attribute declaration syntax 2016-08-12 15:36:12 -07:00
xrewrite1.lean chore(tests/lean/run): make sure tests only use init and system.IO 2016-08-11 18:13:00 -07:00