| .. |
|
expensive
|
|
|
|
extra
|
chore(library/init/reserved_notation): add <= and >=
|
2016-07-09 14:03:05 -07:00 |
|
hott
|
|
|
|
interactive
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
perf
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
run
|
feat(frontends/lean/parser): _ is an anonymous variable again in patterns.
|
2016-08-23 14:06:24 -07:00 |
|
slow
|
chore(library): disable stdlib but init and systems folder
|
2016-08-11 18:42:10 -07:00 |
|
smt2
|
test(frontends/smt2): basic tests for parser and elaborator
|
2016-07-29 10:44:44 -07:00 |
|
trust0
|
|
|
|
trust10
|
refactor(simplifier): many fixes, extensions, and tests
|
2016-08-19 14:57:03 -07:00 |
|
480.hlean
|
|
|
|
480.hlean.expected.out
|
|
|
|
487.hlean
|
|
|
|
487.hlean.expected.out
|
|
|
|
531.hlean
|
|
|
|
531.hlean.expected.out
|
|
|
|
582.hlean
|
|
|
|
582.hlean.expected.out
|
|
|
|
584a.lean
|
|
|
|
584a.lean.expected.out
|
|
|
|
584b.lean
|
|
|
|
584b.lean.expected.out
|
|
|
|
584c.lean
|
|
|
|
584c.lean.expected.out
|
|
|
|
604.lean
|
|
|
|
604.lean.expected.out
|
|
|
|
608.hlean
|
|
|
|
608.hlean.expected.out
|
|
|
|
626a.lean
|
|
|
|
626a.lean.expected.out
|
|
|
|
626b.hlean
|
|
|
|
626b.hlean.expected.out
|
|
|
|
626c.lean
|
|
|
|
626c.lean.expected.out
|
|
|
|
634.lean
|
|
|
|
634.lean.expected.out
|
|
|
|
634b.lean
|
|
|
|
634b.lean.expected.out
|
|
|
|
634c.lean
|
|
|
|
634c.lean.expected.out
|
|
|
|
634d.lean
|
|
|
|
634d.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
640.hlean
|
|
|
|
640.hlean.expected.out
|
|
|
|
640a.hlean
|
|
|
|
640a.hlean.expected.out
|
|
|
|
640b.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
640b.lean.expected.out
|
|
|
|
652.lean
|
|
|
|
652.lean.expected.out
|
|
|
|
671.lean
|
|
|
|
671.lean.expected.out
|
|
|
|
690.hlean
|
|
|
|
690.hlean.expected.out
|
|
|
|
712.lean
|
|
|
|
712.lean.expected.out
|
feat(frontends/lean): quoted names
|
2016-07-22 19:06:57 -07:00 |
|
770.hlean
|
|
|
|
770.hlean.expected.out
|
|
|
|
778.hlean
|
|
|
|
778.hlean.expected.out
|
|
|
|
779.hlean
|
|
|
|
779.hlean.expected.out
|
|
|
|
852.hlean
|
|
|
|
852.hlean.expected.out
|
|
|
|
858.lean
|
|
|
|
858.lean.expected.out
|
feat(frontends/lean/decl_cmds): use new elaborator for variable, parameter and constant commands
|
2016-08-03 17:10:45 -07:00 |
|
893.hlean
|
|
|
|
893.hlean.expected.out
|
|
|
|
abbrev1.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
abbrev1.lean.expected.out
|
|
|
|
abbrev2.lean
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
abbrev2.lean.expected.out
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
abbrev_paren.hlean
|
|
|
|
abbrev_paren.hlean.expected.out
|
|
|
|
acc.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
acc.lean.expected.out
|
chore(tests/lean): fix tests output
|
2016-07-26 17:54:30 -07:00 |
|
acc_rec_bug.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
acc_rec_bug.lean.expected.out
|
|
|
|
alias.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
alias.lean.expected.out
|
|
|
|
alias2.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
alias2.lean.expected.out
|
|
|
|
anc1.lean
|
feat(frontends/lean/elaborator): chaining for anonymous constructors
|
2016-08-04 15:08:25 -07:00 |
|
anc1.lean.expected.out
|
feat(frontends/lean/elaborator): chaining for anonymous constructors
|
2016-08-04 15:08:25 -07:00 |
|
assert_tac3.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
assert_tac3.lean.expected.out
|
fix(frontends/lean/pp): purify metavar_decl_ref's
|
2016-07-30 20:30:03 -07:00 |
|
attributes.lean
|
feat(frontends/lean/decl_attributes): disallow persistent attribute removal
|
2016-08-23 14:09:35 -07:00 |
|
attributes.lean.expected.out
|
feat(frontends/lean/decl_attributes): disallow persistent attribute removal
|
2016-08-23 14:09:35 -07:00 |
|
bad_end.lean
|
|
|
|
bad_end.lean.expected.out
|
|
|
|
bad_id.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
bad_id.lean.expected.out
|
|
|
|
bad_inaccessible.lean
|
feat(frontends/lean/parser): _ is an anonymous variable again in patterns.
|
2016-08-23 14:06:24 -07:00 |
|
bad_inaccessible.lean.expected.out
|
feat(frontends/lean/parser): _ is an anonymous variable again in patterns.
|
2016-08-23 14:06:24 -07:00 |
|
bad_notation.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
bad_notation.lean.expected.out
|
|
|
|
bad_open.lean
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
bad_open.lean.expected.out
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
bad_pattern2.lean
|
feat(frontends/lean/decl_cmds): pattern variables must be atomic
|
2016-06-29 07:34:36 +01:00 |
|
bad_pattern2.lean.expected.out
|
feat(frontends/lean): new pattern matching validation
|
2016-08-07 11:31:11 -07:00 |
|
bad_print.lean
|
|
|
|
bad_print.lean.expected.out
|
|
|
|
bad_quoted_symbol.lean
|
feat(frontends/lean): quoted names
|
2016-07-22 19:06:57 -07:00 |
|
bad_quoted_symbol.lean.expected.out
|
feat(frontends/lean): quoted names
|
2016-07-22 19:06:57 -07:00 |
|
bad_set_option.lean
|
|
|
|
bad_set_option.lean.expected.out
|
|
|
|
bad_structures.lean
|
|
|
|
bad_structures.lean.expected.out
|
|
|
|
bad_structures2.lean
|
|
|
|
bad_structures2.lean.expected.out
|
|
|
|
bug1.lean
|
|
|
|
bug1.lean.expected.out
|
chore(tests/lean): fix tests output
|
2016-07-26 17:54:30 -07:00 |
|
by_contradiction.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
by_contradiction.lean.expected.out
|
fix(library): remove classical instances from global scope
|
2016-07-29 23:44:23 -04:00 |
|
calc1.lean
|
feat(frontends/lean/elaborator): modify the pre-term for overloaded notation
|
2016-07-31 17:14:01 -07:00 |
|
calc1.lean.expected.out
|
feat(frontends/lean/elaborator): modify the pre-term for overloaded notation
|
2016-07-31 17:14:01 -07:00 |
|
cases_failure.hlean
|
|
|
|
cases_failure.hlean.expected.out
|
|
|
|
change1.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
change1.lean.expected.out
|
|
|
|
change2.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
change2.lean.expected.out
|
|
|
|
char_lits.lean
|
feat(frontends/lean): add support for character literals
|
2016-07-18 14:07:10 -04:00 |
|
char_lits.lean.expected.out
|
chore(library/equations_compiler/elim_match): fix style and test output
|
2016-08-18 18:09:36 -07:00 |
|
check.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
check.lean.expected.out
|
fix(frontends/lean/builtin_cmds): non-determinism
|
2016-08-11 08:01:44 -07:00 |
|
check2.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
check2.lean.expected.out
|
fix(frontends/lean/builtin_cmds): non-determinism
|
2016-08-11 08:01:44 -07:00 |
|
choice_expl.lean
|
feat(frontends/lean/builtin_exprs): simplify '@' and '@@'
|
2016-07-02 11:08:18 +01:00 |
|
choice_expl.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
cls_err.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
cls_err.lean.expected.out
|
|
|
|
coe1.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
coe1.lean.expected.out
|
test(tests/lean/coe1): add coercion tests
|
2016-07-30 12:29:12 -07:00 |
|
coe2.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
coe2.lean.expected.out
|
feat(frontends/lean/pp): add option for hiding coercions
|
2016-07-30 12:25:18 -07:00 |
|
coe3.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
coe3.lean.expected.out
|
fix(library/type_context): bug in type class resolution
|
2016-07-30 15:54:28 -07:00 |
|
coe4.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
coe4.lean.expected.out
|
feat(frontends/lean/elaborator): coercions to functions
|
2016-07-30 18:54:20 -07:00 |
|
coe5.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
coe5.lean.expected.out
|
feat(frontends/lean/elaborator): coercions to functions
|
2016-07-30 18:54:20 -07:00 |
|
coe6.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
coe6.lean.expected.out
|
feat(frontends/lean/elaborator): coercions to sort
|
2016-07-30 19:47:04 -07:00 |
|
combinators1.lean
|
feat(library/init/meta/tactic): add 'focus', 'first', 'solve' and LCF-style AND_THEN tactical
|
2016-06-29 01:07:41 +01:00 |
|
combinators1.lean.expected.out
|
feat(library/init/meta/tactic): add 'focus', 'first', 'solve' and LCF-style AND_THEN tactical
|
2016-06-29 01:07:41 +01:00 |
|
config.hlean
|
|
|
|
config.hlean.expected.out
|
|
|
|
config.lean
|
|
|
|
config.lean.expected.out
|
|
|
|
const.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
const.lean.expected.out
|
|
|
|
crash.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
crash.lean.expected.out
|
chore(library/pp_options): remove option pp.metavar_args
|
2016-07-31 16:00:21 -07:00 |
|
ctx.lean
|
|
|
|
ctx.lean.expected.out
|
|
|
|
ctxopt.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
ctxopt.lean.expected.out
|
|
|
|
def1.lean
|
fix(frontends/lean/elaborator): improve error message for eliminator elaborator
|
2016-08-13 15:43:44 -07:00 |
|
def1.lean.expected.out
|
fix(frontends/lean/elaborator): improve error message for eliminator elaborator
|
2016-08-13 15:43:44 -07:00 |
|
def2.lean
|
feat(frontends/lean/definition_cmds): check noncomputable annotation
|
2016-08-13 16:33:02 -07:00 |
|
def2.lean.expected.out
|
feat(frontends/lean/definition_cmds): check noncomputable annotation
|
2016-08-13 16:33:02 -07:00 |
|
def3.lean
|
feat(frontends/lean/definition_cmds): postprocessing for parameters
|
2016-08-13 17:41:05 -07:00 |
|
def3.lean.expected.out
|
feat(frontends/lean/definition_cmds): postprocessing for parameters
|
2016-08-13 17:41:05 -07:00 |
|
def4.lean
|
feat(frontends/lean/definition_cmds): postprocessing for parameters
|
2016-08-13 17:41:05 -07:00 |
|
def4.lean.expected.out
|
feat(frontends/lean/definition_cmds): postprocessing for parameters
|
2016-08-13 17:41:05 -07:00 |
|
defeq1.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
defeq1.lean.expected.out
|
|
|
|
defeq_simp1.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
defeq_simp1.lean.expected.out
|
|
|
|
defeq_simp2.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
defeq_simp2.lean.expected.out
|
chore(tests/lean): fix tests output
|
2016-07-26 17:54:30 -07:00 |
|
defeq_simp_lemmas1.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
defeq_simp_lemmas1.lean.expected.out
|
feat(frontends/lean/pp): improve purify_metavars
|
2016-07-30 15:31:06 -07:00 |
|
defeq_simp_lemmas2.lean
|
chore(library, tests): use new attribute chaining syntax
|
2016-08-16 13:49:03 -07:00 |
|
defeq_simp_lemmas2.lean.expected.out
|
feat(frontends/lean/pp): improve purify_metavars
|
2016-07-30 15:31:06 -07:00 |
|
elab1.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab1.lean.expected.out
|
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
|
2016-07-27 15:29:25 -07:00 |
|
elab2.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab2.lean.expected.out
|
fix(frontends/lean/pp): purify metavar_decl_ref's
|
2016-07-30 20:30:03 -07:00 |
|
elab3.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab3.lean.expected.out
|
chore(tests/lean): fix tests
|
2016-08-04 19:17:08 -07:00 |
|
elab4.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab4.lean.expected.out
|
fix(frontends/lean/elaborator): order type class instances are synthesized
|
2016-08-01 23:59:22 -07:00 |
|
elab4b.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab4b.lean.expected.out
|
fix(frontends/lean/elaborator): order type class instances are synthesized
|
2016-08-01 23:59:22 -07:00 |
|
elab5.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab5.lean.expected.out
|
test(tests/lean): more examples
|
2016-07-27 16:08:33 -07:00 |
|
elab6.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab6.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
elab7.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab7.lean.expected.out
|
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
|
2016-07-27 15:29:25 -07:00 |
|
elab8.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab8.lean.expected.out
|
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
|
2016-07-27 15:29:25 -07:00 |
|
elab9.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab9.lean.expected.out
|
test(tests/lean): more examples
|
2016-07-27 16:08:33 -07:00 |
|
elab11.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab11.lean.expected.out
|
refactor(frontends/lean/elaborator): snapshots
|
2016-07-29 10:36:14 -07:00 |
|
elab12.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab12.lean.expected.out
|
feat(frontends/lean/elaborator): coercions to functions
|
2016-07-30 18:54:20 -07:00 |
|
elab13.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab13.lean.expected.out
|
fix(frontends/lean/elaborator): check expected type in applications, make sure we don't accidentally unfold definitions unnecessarily
|
2016-07-28 17:30:56 -07:00 |
|
elab14.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab14.lean.expected.out
|
feat(frontends/lean/elaborator): convert unassigned universe levels into universe parameters, basic support for by tactic
|
2016-07-31 03:45:18 -07:00 |
|
elab15.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
elab15.lean.expected.out
|
feat(frontends/lean/elaborator): invoke tactics
|
2016-07-31 11:56:52 -07:00 |
|
empty.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
empty.lean.expected.out
|
|
|
|
error_full_names.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
error_full_names.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
errors2.lean
|
|
|
|
errors2.lean.expected.out
|
|
|
|
eta_bug.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
eta_bug.lean.expected.out
|
refactor(library): remove eq.ops namespace
|
2016-07-31 12:50:11 -07:00 |
|
eta_tac.lean
|
feat(library/type_context, library/tactic): add eta-expansion method and tactic
|
2016-08-14 16:15:12 -07:00 |
|
eta_tac.lean.expected.out
|
feat(library/type_context, library/tactic): add eta-expansion method and tactic
|
2016-08-14 16:15:12 -07:00 |
|
focus_tac.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
focus_tac.lean.expected.out
|
fix(frontends/lean/pp): purify metavar_decl_ref's
|
2016-07-30 20:30:03 -07:00 |
|
fold.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
fold.lean.expected.out
|
|
|
|
format_thunk1.lean
|
feat(library/vm/vm_format,library/tactic): use thunks unit->format when producing error messages
|
2016-08-04 19:19:09 -07:00 |
|
format_thunk1.lean.expected.out
|
feat(library/vm/vm_format,library/tactic): use thunks unit->format when producing error messages
|
2016-08-04 19:19:09 -07:00 |
|
ftree.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
ftree.lean.expected.out
|
chore(tests/lean): fix test output
|
2016-08-03 14:17:29 -07:00 |
|
generalize1.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
generalize1.lean.expected.out
|
chore(tests/lean): fix tests output
|
2016-07-26 17:54:30 -07:00 |
|
hex_char.lean
|
feat(frontends/lean/scanner): hex scape in character literal
|
2016-07-19 12:38:20 -04:00 |
|
hex_char.lean.expected.out
|
feat(frontends/lean/scanner): hex scape in character literal
|
2016-07-19 12:38:20 -04:00 |
|
hex_numeral.lean
|
feat(frontends/lean/scanner): hexadecimal numerals
|
2016-07-19 13:04:27 -04:00 |
|
hex_numeral.lean.expected.out
|
feat(frontends/lean/scanner): hexadecimal numerals
|
2016-07-19 13:04:27 -04:00 |
|
inaccessible.lean
|
feat(frontends/lean/parser): _ is an anonymous variable again in patterns.
|
2016-08-23 14:06:24 -07:00 |
|
inaccessible.lean.expected.out
|
feat(frontends/lean): revising inaccessible terms syntax again :(
|
2016-08-19 13:57:12 -07:00 |
|
induction_tac1.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
induction_tac1.lean.expected.out
|
feat(library/tactic/induction_tactic): clear major premise
|
2016-07-07 07:39:25 -07:00 |
|
inductive_cmd_leftover_placeholder_universe.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
inductive_cmd_leftover_placeholder_universe.lean.expected.out
|
|
|
|
inst.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
inst.lean.expected.out
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
inst_error.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
inst_error.lean.expected.out
|
chore(tests/lean/inst_error.lean.expected.out): fix output
|
2016-08-02 13:55:08 -07:00 |
|
internal_names.lean
|
|
|
|
internal_names.lean.expected.out
|
|
|
|
key_eqv1.lean
|
feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences'
|
2016-07-16 15:41:32 -04:00 |
|
key_eqv1.lean.expected.out
|
feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences'
|
2016-07-16 15:41:32 -04:00 |
|
let1.lean
|
|
|
|
let1.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
let3.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
let3.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
let4.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
let4.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
lift_coe_off.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
lift_coe_off.lean.expected.out
|
|
|
|
list_monad1.lean
|
feat(library/init): add 'guard' and helper typeclasses
|
2016-07-07 00:52:52 -07:00 |
|
list_monad1.lean.expected.out
|
feat(library/init): add 'guard' and helper typeclasses
|
2016-07-07 00:52:52 -07:00 |
|
local_notation_bug2.lean
|
|
|
|
local_notation_bug2.lean.expected.out
|
|
|
|
match_bug.lean
|
|
|
|
match_bug.lean.expected.out
|
fix(frontends/lean/match_expr): nary match revision
|
2016-08-10 07:24:10 -07:00 |
|
mismatch.lean
|
|
|
|
mismatch.lean.expected.out
|
|
|
|
namespace_bug.lean
|
|
|
|
namespace_bug.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
nary_overload.lean
|
|
|
|
nary_overload.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
nat_pp.lean
|
|
|
|
nat_pp.lean.expected.out
|
|
|
|
nested1.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
nested1.lean.expected.out
|
chore(frontends/lean/print_cmd): change attribute output to new syntax
|
2016-08-16 13:49:03 -07:00 |
|
no_confusion_type.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
no_confusion_type.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
noncomp.lean
|
|
|
|
noncomp.lean.expected.out
|
|
|
|
noncomp_error.lean
|
|
|
|
noncomp_error.lean.expected.out
|
|
|
|
noncomp_hott.hlean
|
|
|
|
noncomp_hott.hlean.expected.out
|
|
|
|
noncomp_thm.lean
|
|
|
|
noncomp_thm.lean.expected.out
|
|
|
|
notation.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
notation.lean.expected.out
|
|
|
|
notation2.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
notation2.lean.expected.out
|
|
|
|
notation3.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
notation3.lean.expected.out
|
|
|
|
notation4.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
notation4.lean.expected.out
|
|
|
|
notation5.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
notation5.lean.expected.out
|
|
|
|
notation6.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
notation6.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
notation7.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
notation7.lean.expected.out
|
|
|
|
notation8.lean
|
fix(library/init/function): '$' notation should be left-associative
|
2016-08-09 16:50:36 -07:00 |
|
notation8.lean.expected.out
|
fix(library/init/function): '$' notation should be left-associative
|
2016-08-09 16:50:36 -07:00 |
|
num.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
num.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
num2.lean
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
num2.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
num3.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
num3.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
num4.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
num4.lean.expected.out
|
|
|
|
num5.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
num5.lean.expected.out
|
|
|
|
omit.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
omit.lean.expected.out
|
|
|
|
over_notation.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
over_notation.lean.expected.out
|
feat(frontends/lean/elaborator): modify the pre-term for overloaded notation
|
2016-07-31 17:14:01 -07:00 |
|
param.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
param.lean.expected.out
|
|
|
|
param_binder_update.lean
|
|
|
|
param_binder_update.lean.expected.out
|
|
|
|
param_binder_update2.lean
|
|
|
|
param_binder_update2.lean.expected.out
|
|
|
|
parsing_only.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
parsing_only.lean.expected.out
|
|
|
|
pattern_pp.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
pattern_pp.lean.expected.out
|
chore(frontends/lean/print_cmd): change attribute output to new syntax
|
2016-08-16 13:49:03 -07:00 |
|
pp.lean
|
|
|
|
pp.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
pp_all.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
pp_all.lean.expected.out
|
chore(library/class): disable [trans_instance] attribute
|
2016-07-29 23:28:36 -07:00 |
|
pp_all2.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
pp_all2.lean.expected.out
|
chore(tests/lean/pp_all2): fix test output
|
2016-07-29 23:35:10 -07:00 |
|
pp_beta.lean
|
|
|
|
pp_beta.lean.expected.out
|
|
|
|
pp_binder_types.lean
|
|
|
|
pp_binder_types.lean.expected.out
|
|
|
|
pp_bug.lean
|
|
|
|
pp_bug.lean.expected.out
|
|
|
|
pp_no_proofs.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
pp_no_proofs.lean.expected.out
|
feat(frontends/lean): revising inaccessible terms syntax again :(
|
2016-08-19 13:57:12 -07:00 |
|
pp_param_bug.lean
|
|
|
|
pp_param_bug.lean.expected.out
|
|
|
|
ppbug.lean
|
|
|
|
ppbug.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
print_ax1.lean
|
|
|
|
print_ax1.lean.expected.out
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
print_ax2.lean
|
|
|
|
print_ax2.lean.expected.out
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
print_ax3.lean
|
|
|
|
print_ax3.lean.expected.out
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
print_reducible.lean
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
print_reducible.lean.expected.out
|
|
|
|
print_thm.lean
|
|
|
|
print_thm.lean.expected.out
|
|
|
|
private_structure.lean
|
feat(frontends/lean/structure_cmd): private structures
|
2016-08-06 00:03:06 -07:00 |
|
private_structure.lean.expected.out
|
fix(frontends/lean/builtin_cmds): non-determinism
|
2016-08-11 08:01:44 -07:00 |
|
prodtst.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
prodtst.lean.expected.out
|
|
|
|
protected.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
protected.lean.expected.out
|
|
|
|
protected_consts.lean
|
|
|
|
protected_consts.lean.expected.out
|
|
|
|
protected_test.lean
|
|
|
|
protected_test.lean.expected.out
|
fix(frontends/lean/builtin_cmds): non-determinism
|
2016-08-11 08:01:44 -07:00 |
|
qexpr1.lean
|
feat(library/tactic, frontends/lean/elaborator): add to_expr tactic
|
2016-07-31 20:21:17 -07:00 |
|
qexpr1.lean.expected.out
|
feat(library/tactic, frontends/lean/elaborator): add to_expr tactic
|
2016-07-31 20:21:17 -07:00 |
|
qexpr2.lean
|
fix(library/tactic/elaborate): new subgoals must be inserted after main goal
|
2016-07-31 21:16:29 -07:00 |
|
qexpr2.lean.expected.out
|
feat(library/tactic/elaborate): convert unassigned metavars into new goals
|
2016-07-31 20:38:57 -07:00 |
|
qexpr3.lean
|
feat(library/init/meta/tactic): add 'refine' tactic
|
2016-07-31 21:17:19 -07:00 |
|
qexpr3.lean.expected.out
|
feat(library/init/meta/tactic): add 'refine' tactic
|
2016-07-31 21:17:19 -07:00 |
|
quot_bug.lean
|
|
|
|
quot_bug.lean.expected.out
|
|
|
|
quot_ind_bug.lean
|
|
|
|
quot_ind_bug.lean.expected.out
|
|
|
|
record_rec_protected.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
record_rec_protected.lean.expected.out
|
|
|
|
red.lean
|
|
|
|
red.lean.expected.out
|
chore(library/pp_options): remove option pp.metavar_args
|
2016-07-31 16:00:21 -07:00 |
|
reserve_bugs.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
reserve_bugs.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
restrict_bug.lean
|
feat(library/type_context): restrict context of metavariables during unification if approximate() is true
|
2016-08-02 16:31:12 -07:00 |
|
restrict_bug.lean.expected.out
|
feat(library/type_context): restrict context of metavariables during unification if approximate() is true
|
2016-08-02 16:31:12 -07:00 |
|
rev_tac1.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
rev_tac1.lean.expected.out
|
chore(tests/lean): fix tests output
|
2016-07-26 17:54:30 -07:00 |
|
rquote.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
rquote.lean.expected.out
|
feat(frontends/lean): resolved quoted names
|
2016-08-05 17:04:36 -07:00 |
|
sec.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
sec.lean.expected.out
|
|
|
|
sec3.lean
|
|
|
|
sec3.lean.expected.out
|
|
|
|
sec_param_pp.lean
|
|
|
|
sec_param_pp.lean.expected.out
|
|
|
|
sec_param_pp2.lean
|
|
|
|
sec_param_pp2.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
set_opt_tac.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
set_opt_tac.lean.expected.out
|
|
|
|
shadow.lean
|
|
|
|
shadow.lean.expected.out
|
feat(frontends/lean): new pattern matching validation
|
2016-08-07 11:31:11 -07:00 |
|
showenv.l
|
|
|
|
simp_idp.hlean
|
|
|
|
simp_idp.hlean.expected.out
|
|
|
|
simplifier1.hlean
|
|
|
|
simplifier1.hlean.expected.out
|
|
|
|
simplifier_prove_failures.lean
|
refactor(simplifier): many fixes, extensions, and tests
|
2016-08-19 14:57:03 -07:00 |
|
simplifier_prove_failures.lean.expected.out
|
refactor(simplifier): many fixes, extensions, and tests
|
2016-08-19 14:57:03 -07:00 |
|
simplifier_unsafe_nary.lean
|
refactor(simplifier): many fixes, extensions, and tests
|
2016-08-19 14:57:03 -07:00 |
|
simplifier_unsafe_nary.lean.expected.out
|
refactor(simplifier): many fixes, extensions, and tests
|
2016-08-19 14:57:03 -07:00 |
|
struct_class.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
struct_class.lean.expected.out
|
refactor(simplifier): many fixes, extensions, and tests
|
2016-08-19 14:57:03 -07:00 |
|
structure_result_type_may_be_zero.lean
|
|
|
|
structure_result_type_may_be_zero.lean.expected.out
|
|
|
|
structure_with_index_error.lean
|
|
|
|
structure_with_index_error.lean.expected.out
|
|
|
|
subpp.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
subpp.lean.expected.out
|
chore(tests/lean): adjust tests
|
2016-07-23 12:48:35 -07:00 |
|
subst_bug.lean
|
fix(library/tactic/subst_tactic): incorrect depends_on
|
2016-08-16 11:19:06 -07:00 |
|
subst_bug.lean.expected.out
|
fix(library/tactic/subst_tactic): incorrect depends_on
|
2016-08-16 11:19:06 -07:00 |
|
substvars2.hlean
|
|
|
|
substvars2.hlean.expected.out
|
|
|
|
t2.lean
|
|
|
|
t2.lean.expected.out
|
|
|
|
t3.lean
|
|
|
|
t3.lean.expected.out
|
|
|
|
t5.lean
|
|
|
|
t5.lean.expected.out
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
t6.lean
|
|
|
|
t6.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
t10.lean
|
|
|
|
t10.lean.expected.out
|
|
|
|
t11.lean
|
|
|
|
t11.lean.expected.out
|
|
|
|
t12.lean
|
|
|
|
t12.lean.expected.out
|
|
|
|
t13.lean
|
|
|
|
t13.lean.expected.out
|
feat(frontends/lean/elaborator): modify the pre-term for overloaded notation
|
2016-07-31 17:14:01 -07:00 |
|
t14.lean
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
t14.lean.expected.out
|
feat(frontends/lean, library): remove attribute and metaclass scoping
|
2016-07-29 23:44:21 -04:00 |
|
tactic_failure.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
tactic_failure.lean.expected.out
|
|
|
|
test.sh
|
|
|
|
test_single.sh
|
|
|
|
test_single_pp.sh
|
|
|
|
trace1.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
trace1.lean.expected.out
|
feat(library/init/meta/tactic): add 'when_tracing' tactical
|
2016-06-28 11:29:39 +01:00 |
|
trace2.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
trace2.lean.expected.out
|
feat(frontends/lean): add declare_trace command
|
2016-06-28 11:45:56 +01:00 |
|
tuple.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
tuple.lean.expected.out
|
|
|
|
type_class_bug.lean
|
feat(frontends/lean): remove #elab command
|
2016-08-02 15:05:24 -07:00 |
|
type_class_bug.lean.expected.out
|
fix(library/metavar_util): but in instantiate_mvars
|
2016-08-02 13:16:17 -07:00 |
|
unfold1.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
unfold1.lean.expected.out
|
feat(library/tactic): add unfold tactic
|
2016-07-18 15:46:56 -04:00 |
|
unfold4.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
unfold4.lean.expected.out
|
fix(library/tactic/unfold_tactic): should use type_context locals
|
2016-07-18 19:08:31 -04:00 |
|
unfold_crash.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
unfold_crash.lean.expected.out
|
fix(library/tactic/unfold_crash): crash when constant is not a definition
|
2016-07-18 19:59:17 -04:00 |
|
unfold_crash2.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
unfold_crash2.lean.expected.out
|
feat(library/tactic/unfold_tactic): improve fold failure detection
|
2016-07-18 20:17:40 -04:00 |
|
uni_bug1.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
uni_bug1.lean.expected.out
|
refactor(library): move 'none', 'some', 'tt', 'ff' to top-level
|
2016-06-25 12:39:19 -07:00 |
|
unification_hints1.lean
|
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
|
2016-08-17 07:34:03 -07:00 |
|
unification_hints1.lean.expected.out
|
chore(library, tests): switch to new attribute declaration syntax
|
2016-08-12 15:36:12 -07:00 |
|
unifier_bug.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
unifier_bug.lean.expected.out
|
|
|
|
unify3.lean
|
chore(frontends/lean): coercions are disabled by default
|
2016-07-29 13:03:23 -07:00 |
|
unify3.lean.expected.out
|
fix(frontends/lean/pp): purify metavar_decl_ref's
|
2016-07-30 20:30:03 -07:00 |
|
unify_tac1.lean
|
feat(library/tactic/tactic_state): add is_def_eq and is_def_eq_core tactics
|
2016-08-16 11:08:03 -07:00 |
|
unify_tac1.lean.expected.out
|
feat(library/tactic/tactic_state): add is_def_eq and is_def_eq_core tactics
|
2016-08-16 11:08:03 -07:00 |
|
univ.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
univ.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
univ_vars.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
univ_vars.lean.expected.out
|
feat(frontends/lean/elaborator): universe parameter name sanitizer
|
2016-08-03 13:13:44 -07:00 |
|
user_attribute.lean
|
feat(library/vm/user_attribute): use command instead of attribute for registering
|
2016-08-18 15:51:41 -07:00 |
|
user_attribute.lean.expected.out
|
fix(tests/lean/user_attribute): test output
|
2016-08-18 15:55:55 -07:00 |
|
utf8.lean
|
feat(library/init/string): add utf8_length
|
2016-07-19 14:22:37 -04:00 |
|
utf8.lean.expected.out
|
feat(library/init/string): add utf8_length
|
2016-07-19 14:22:37 -04:00 |
|
var.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
var.lean.expected.out
|
|
|
|
var2.lean
|
chore(tests/lean): make sure tests only use init and systems.IO
|
2016-08-11 18:31:33 -07:00 |
|
var2.lean.expected.out
|
|
|
|
vm_eval_crash.lean
|
fix(frontends/lean/builtin_cmds): fail if expression contain metavars
|
2016-07-19 13:22:10 -04:00 |
|
vm_eval_crash.lean.expected.out
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
whnf.lean
|
feat(frontends/lean): use new elaborator in the 'check' command
|
2016-08-02 14:57:49 -07:00 |
|
whnf.lean.expected.out
|
|
|
|
whnf_cache_bug.lean
|
fix(library/type_context): whnf cache bug
|
2016-08-18 18:04:19 -07:00 |
|
whnf_cache_bug.lean.expected.out
|
fix(library/type_context): whnf cache bug
|
2016-08-18 18:04:19 -07:00 |
|
whnf_core1.lean
|
feat(library/tactic/tactic_state): add whnf_core
|
2016-08-14 16:02:40 -07:00 |
|
whnf_core1.lean.expected.out
|
feat(library/tactic/tactic_state): add whnf_core
|
2016-08-14 16:02:40 -07:00 |
