| .. |
|
expensive
|
chore(tests/lean): add 'expensive' file
|
2014-08-01 10:35:32 -07:00 |
|
extra
|
test(tests/lean/extra): add regression tests for issue #422
|
2015-02-04 10:55:03 -08:00 |
|
hott
|
feat(library/tactic/rewrite_tactic): allow rewrite with terms that contains binders
|
2015-03-12 18:07:55 -07:00 |
|
interactive
|
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
|
2015-03-13 14:47:21 -07:00 |
|
run
|
fix(library/tactic/inversion_tactic): missing condition for applying optimization
|
2015-03-12 09:11:36 -07:00 |
|
slow
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
trust0
|
feat(shell): set default behavior to "trusted"
|
2015-01-21 16:25:09 -08:00 |
|
438.lean
|
refactor(library/algebra): move bundled structures to separate module
|
2015-03-02 18:45:08 -08:00 |
|
438.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
abbrev1.lean
|
test(tests/lean/abbrev1): add test for abbreviation command
|
2015-02-10 18:28:48 -08:00 |
|
abbrev1.lean.expected.out
|
test(tests/lean/abbrev1): add test for abbreviation command
|
2015-02-10 18:28:48 -08:00 |
|
abbrev2.lean
|
fix(frontends/lean/pp): bugs when pretty printing abbreviations
|
2015-02-10 19:06:09 -08:00 |
|
abbrev2.lean.expected.out
|
fix(frontends/lean/pp): bugs when pretty printing abbreviations
|
2015-02-10 19:06:09 -08:00 |
|
acc.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
acc.lean.expected.out
|
feat(kernel/inductive): relax conditions for an inductive datatype in Prop to be able to eliminate into Type
|
2014-11-06 09:36:54 -08:00 |
|
acc_rec_bug.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
acc_rec_bug.lean.expected.out
|
fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop
|
2014-11-06 14:03:28 -08:00 |
|
alias.lean
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
|
2014-10-02 17:55:34 -07:00 |
|
alias.lean.expected.out
|
feat(frontends/lean): add basic pretty printer
|
2014-07-09 01:12:36 -07:00 |
|
alias2.lean
|
fix(frontends/lean/pp): pp was not taking into account new namespace name resolution rules, fixes #216
|
2014-10-01 11:24:45 -07:00 |
|
alias2.lean.expected.out
|
fix(frontends/lean/pp): pp was not taking into account new namespace name resolution rules, fixes #216
|
2014-10-01 11:24:45 -07:00 |
|
apply_fail.lean
|
feat(library/tactic): produce better error message when a tactic fails
|
2015-02-16 18:42:15 -08:00 |
|
apply_fail.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
assert_fail.lean
|
feat(frontends/lean): add 'assert H : A, ...' as notation for 'have H [visible] : A, ...'
|
2015-02-25 14:30:42 -08:00 |
|
assert_fail.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
bad_class.lean
|
refactor(frontends/lean): add 'attribute' command
|
2015-01-24 20:23:21 -08:00 |
|
bad_class.lean.expected.out
|
fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests
|
2014-10-08 23:44:09 -07:00 |
|
bad_coercions.lean
|
refactor(frontends/lean): add 'attribute' command
|
2015-01-24 20:23:21 -08:00 |
|
bad_coercions.lean.expected.out
|
refactor(frontends/lean): add 'attribute' command
|
2015-01-24 20:23:21 -08:00 |
|
bad_end.lean
|
fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244
|
2014-10-13 21:08:36 -07:00 |
|
bad_end.lean.expected.out
|
fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244
|
2014-10-13 21:08:36 -07:00 |
|
bad_eqns.lean
|
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
|
2015-03-13 14:47:21 -07:00 |
|
bad_eqns.lean.expected.out
|
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
|
2015-03-13 14:47:21 -07:00 |
|
bad_id.lean
|
feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1'
|
2014-11-09 12:55:13 -08:00 |
|
bad_id.lean.expected.out
|
feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1'
|
2014-11-09 12:55:13 -08:00 |
|
bad_namespace.lean
|
test(tests/lean): add more tests for error messages
|
2015-02-01 20:04:22 -08:00 |
|
bad_namespace.lean.expected.out
|
test(tests/lean): add more tests for error messages
|
2015-02-01 20:04:22 -08:00 |
|
bad_notation.lean
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
bad_notation.lean.expected.out
|
feat(frontends/lean/notation_cmd): remove the cleanup notation hack
|
2014-10-11 16:40:26 -07:00 |
|
bad_open.lean
|
test(tests/lean): add more tests for error messages
|
2015-02-01 20:04:22 -08:00 |
|
bad_open.lean.expected.out
|
test(tests/lean): add more tests for error messages
|
2015-02-01 20:04:22 -08:00 |
|
bad_print.lean
|
test(tests/lean): add more tests for error messages
|
2015-02-01 20:04:22 -08:00 |
|
bad_print.lean.expected.out
|
test(tests/lean): add more tests for error messages
|
2015-02-01 20:04:22 -08:00 |
|
bad_set_option.lean
|
test(tests/lean/bad_set_option): add tests for bad 'set_option' command
|
2015-02-01 20:20:35 -08:00 |
|
bad_set_option.lean.expected.out
|
test(tests/lean/bad_set_option): add tests for bad 'set_option' command
|
2015-02-01 20:20:35 -08:00 |
|
bad_structures.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
bad_structures.lean.expected.out
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
bad_structures2.lean
|
test(tests/lean): add tests for structure command error messages
|
2015-01-30 09:52:42 -08:00 |
|
bad_structures2.lean.expected.out
|
test(tests/lean): add tests for structure command error messages
|
2015-01-30 09:52:42 -08:00 |
|
beginend_bug.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
beginend_bug.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
bug1.lean
|
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
|
2015-03-13 14:47:21 -07:00 |
|
bug1.lean.expected.out
|
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
|
2015-03-13 14:47:21 -07:00 |
|
calc1.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
calc1.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
calc_assistant.lean
|
feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option
|
2014-10-31 09:49:45 -07:00 |
|
calc_assistant.lean.expected.out
|
feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option
|
2014-10-31 09:49:45 -07:00 |
|
change_tac_fail.lean
|
refactor(frontends/lean): approach used to parse tactics
|
2015-03-05 18:11:21 -08:00 |
|
change_tac_fail.lean.expected.out
|
refactor(frontends/lean): approach used to parse tactics
|
2015-03-05 18:11:21 -08:00 |
|
check.lean
|
feat(frontends/lean): use nice names for meta-variables when executing check c and c is a constant
|
2014-10-24 08:23:26 -07:00 |
|
check.lean.expected.out
|
feat(frontends/lean): display metavariable application arguments in check command
|
2014-10-30 13:28:25 -07:00 |
|
check2.lean
|
fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming
|
2014-10-26 19:19:45 -07:00 |
|
check2.lean.expected.out
|
feat(frontends/lean): display metavariable application arguments in check command
|
2014-10-30 13:28:25 -07:00 |
|
choice_expl.lean
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
|
2014-10-02 17:55:34 -07:00 |
|
choice_expl.lean.expected.out
|
fix(frontends/lean): distribute '@' over choice
|
2014-08-27 16:31:18 -07:00 |
|
cls_err.lean
|
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
|
2014-10-12 13:06:00 -07:00 |
|
cls_err.lean.expected.out
|
feat(library/tactic/goal): add option pp.compact_goals
|
2014-10-28 16:30:37 -07:00 |
|
coe.lean
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
|
2014-10-02 17:55:34 -07:00 |
|
coe.lean.expected.out
|
fix(frontends/lean/pp): when formatting a coercion to function-class
|
2014-09-20 09:56:46 -07:00 |
|
config.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
config.lean.expected.out
|
chore(shell): re-activate .lean tests
|
2014-06-11 14:36:42 -07:00 |
|
const.lean
|
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
|
2014-10-12 13:06:00 -07:00 |
|
const.lean.expected.out
|
feat(frontends/lean): variables/parameters and check commands have access to all section variables/parameters, closes #231
|
2014-10-08 08:40:55 -07:00 |
|
crash.lean
|
feat(frontends/lean): allow parameters only in contexts
|
2014-10-11 17:13:56 -07:00 |
|
crash.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
ctx.lean
|
feat(library/tactic/goal): when listing context/goal variables, collect vars of same type in one line
|
2015-01-13 11:14:44 -08:00 |
|
ctx.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
ctxopt.lean
|
fix(frontends/lean/parser): configuration options defined in a context are transient, fixes #162
|
2014-09-09 11:02:54 -07:00 |
|
ctxopt.lean.expected.out
|
fix(frontends/lean/parser): configuration options defined in a context are transient, fixes #162
|
2014-09-09 11:02:54 -07:00 |
|
empty.lean
|
feat(frontends/lean): rename 'using' command to 'open'
|
2014-09-03 16:00:38 -07:00 |
|
empty.lean.expected.out
|
feat(library/tactic/goal): add option pp.compact_goals
|
2014-10-28 16:30:37 -07:00 |
|
empty_thm.lean
|
refactor(frontends/lean): approach used to parse tactics
|
2015-03-05 18:11:21 -08:00 |
|
empty_thm.lean.expected.out
|
fix(frontends/lean/decl_cmds): improve error message for invalid end of theorem
|
2014-08-17 17:03:54 -07:00 |
|
error_full_names.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
error_full_names.lean.expected.out
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
error_pos_bug.lean
|
fix(frontends/lean/elaborator): bug when reporting error position
|
2014-10-10 17:31:12 -07:00 |
|
error_pos_bug.lean.expected.out
|
fix(frontends/lean/elaborator): bug when reporting error position
|
2014-10-10 17:31:12 -07:00 |
|
error_pos_bug2.lean
|
fix(frontends/lean/inductive_cmd): bug in expression position propagation, fixes #289
|
2014-11-04 07:44:47 -08:00 |
|
error_pos_bug2.lean.expected.out
|
fix(frontends/lean/inductive_cmd): bug in expression position propagation, fixes #289
|
2014-11-04 07:44:47 -08:00 |
|
errors.lean
|
test(tests/lean): tests for error handling improvements
|
2015-03-13 15:32:25 -07:00 |
|
errors.lean.expected.out
|
test(tests/lean): tests for error handling improvements
|
2015-03-13 15:32:25 -07:00 |
|
eta_bug.lean
|
refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation
|
2015-02-07 15:19:41 -08:00 |
|
eta_bug.lean.expected.out
|
fix(tests/lean): adjust test to new eval semantics
|
2014-11-10 21:10:33 -08:00 |
|
fold.lean
|
refactor(*): modify '|' binding power, use 'abs a' instead of '|a|', and '(a | b)' instead of 'a | b'
|
2015-02-25 15:18:21 -08:00 |
|
fold.lean.expected.out
|
fix(tests/lean): adjust tests to reflect changes in the standard library
|
2015-02-01 11:36:38 -08:00 |
|
ftree.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
ftree.lean.expected.out
|
feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes
|
2014-11-12 10:52:32 -08:00 |
|
gen_bug.lean
|
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
|
2015-03-13 14:47:21 -07:00 |
|
gen_bug.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
gen_fail.lean
|
feat(library/tactic): produce better error message when a tactic fails
|
2015-02-16 18:42:15 -08:00 |
|
gen_fail.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
goals1.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
goals1.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
have1.lean
|
feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included
|
2014-10-22 18:11:09 -07:00 |
|
have1.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
ind_parser_bug.lean
|
fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.
|
2014-11-05 23:12:00 -08:00 |
|
ind_parser_bug.lean.expected.out
|
fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.
|
2014-11-05 23:12:00 -08:00 |
|
inst.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
inst.lean.expected.out
|
feat(frontends/lean): allow user to associate priorities to class-instances, closes #180
|
2014-09-28 12:20:42 -07:00 |
|
inv_del.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
inv_del.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
K_bug.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
K_bug.lean.expected.out
|
fix(kernel/inductive/inductive): fix assertion violation when K is applied to type incorrect term
|
2015-01-27 11:22:14 -08:00 |
|
let1.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
let1.lean.expected.out
|
fix(frontends/lean/pp): pretty print 'let-expressions', closes #87
|
2014-08-28 18:20:58 -07:00 |
|
let3.lean
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
|
2014-10-02 17:55:34 -07:00 |
|
let3.lean.expected.out
|
feat(frontends/lean/pp): improve let-expr pretty printer
|
2014-08-29 07:46:58 -07:00 |
|
let4.lean
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
|
2014-10-02 17:55:34 -07:00 |
|
let4.lean.expected.out
|
fix(frontends/let): let-expression pretty printer
|
2014-08-29 10:58:27 -07:00 |
|
namespace_bug.lean
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
namespace_bug.lean.expected.out
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
nat_pp.lean
|
feat(frontends/lean/pp): add hard-coded pretty printer for nat numerals
|
2014-12-01 16:07:55 -08:00 |
|
nat_pp.lean.expected.out
|
feat(frontends/lean/pp): add hard-coded pretty printer for nat numerals
|
2014-12-01 16:07:55 -08:00 |
|
natsucc.lean
|
feat(frontends/lean): better error messages for ill-terminated declarations
|
2015-02-10 14:38:00 -08:00 |
|
natsucc.lean.expected.out
|
feat(frontends/lean): better error messages for ill-terminated declarations
|
2015-02-10 14:38:00 -08:00 |
|
no_confusion_type.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
no_confusion_type.lean.expected.out
|
fix(tests/lean): to reflect recent changes
|
2014-12-01 17:14:11 -08:00 |
|
nonexhaustive.lean
|
feat(frontends/lean): ML-like notation for match and recursive equations
|
2015-02-25 16:20:44 -08:00 |
|
nonexhaustive.lean.expected.out
|
fix(tests/lean/nonexhaustive): remove line "warning: imported file uses 'sorry'" from test produced output
|
2015-02-01 21:25:52 -08:00 |
|
notation.lean
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
notation.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
notation2.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
notation2.lean.expected.out
|
fix(tests/lean/notation): remove 'sorry' warning from expected outputs
|
2014-10-20 15:34:44 -07:00 |
|
notation3.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
notation3.lean.expected.out
|
fix(tests/lean/notation): remove 'sorry' warning from expected outputs
|
2014-10-20 15:34:44 -07:00 |
|
notation4.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
notation4.lean.expected.out
|
fix(tests/lean/notation): remove 'sorry' warning from expected outputs
|
2014-10-20 15:34:44 -07:00 |
|
notation5.lean
|
feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence
|
2014-10-19 13:39:06 -07:00 |
|
notation5.lean.expected.out
|
feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence
|
2014-10-19 13:39:06 -07:00 |
|
notation6.lean
|
fix(frontends/lean/pp): bug in pretty printer notation match procedure
|
2014-10-20 18:58:27 -07:00 |
|
notation6.lean.expected.out
|
fix(frontends/lean/pp): bug in pretty printer notation match procedure
|
2014-10-20 18:58:27 -07:00 |
|
notation7.lean
|
refactor(library/data/num): break into pieces to reduce dependencies
|
2014-11-07 08:24:29 -08:00 |
|
notation7.lean.expected.out
|
feat(frontends/lean): max precedence used by Lean is not max_uint anymore
|
2014-11-07 07:57:11 -08:00 |
|
num.lean
|
feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
|
2014-09-04 17:26:36 -07:00 |
|
num.lean.expected.out
|
feat(frontends/lean/pp): pretty print numerals
|
2014-08-14 09:12:22 -07:00 |
|
num2.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
num2.lean.expected.out
|
feat(frontends/lean): allow users to define "numeral notation"
|
2014-09-26 14:55:23 -07:00 |
|
num3.lean
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
|
2014-10-02 17:55:34 -07:00 |
|
num3.lean.expected.out
|
feat(frontends/lean): allow users to define "numeral notation"
|
2014-09-26 14:55:23 -07:00 |
|
num4.lean
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
|
2014-10-02 17:55:34 -07:00 |
|
num4.lean.expected.out
|
feat(frontends/lean): allow users to define "numeral notation"
|
2014-09-26 14:55:23 -07:00 |
|
num5.lean
|
fix(frontends/lean): add 'eval' command
|
2014-09-26 20:16:03 -07:00 |
|
num5.lean.expected.out
|
fix(frontends/lean): add 'eval' command
|
2014-09-26 20:16:03 -07:00 |
|
omit.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
omit.lean.expected.out
|
feat(frontends/lean): add 'include' and 'omit' commands, closes #184
|
2014-10-03 07:23:24 -07:00 |
|
open_tst.lean
|
feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command
|
2015-02-11 11:02:59 -08:00 |
|
open_tst.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
param.lean
|
feat(frontends/lean/parser): reject ambiguous parameter declaration, closes #242
|
2014-10-10 18:08:03 -07:00 |
|
param.lean.expected.out
|
feat(frontends/lean/parser): reject ambiguous parameter declaration, closes #242
|
2014-10-10 18:08:03 -07:00 |
|
parsing_only.lean
|
feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305
|
2014-11-06 21:34:05 -08:00 |
|
parsing_only.lean.expected.out
|
feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305
|
2014-11-06 21:34:05 -08:00 |
|
place_eqn.lean
|
feat(frontends/lean): ML-like notation for match and recursive equations
|
2015-02-25 16:20:44 -08:00 |
|
place_eqn.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
pp.lean
|
feat(frontends/lean): pp.beta is true by default
|
2015-02-24 12:27:53 -08:00 |
|
pp.lean.expected.out
|
feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command
|
2014-10-30 13:12:45 -07:00 |
|
pp_beta.lean
|
feat(frontends/lean): pp.beta is true by default
|
2015-02-24 12:27:53 -08:00 |
|
pp_beta.lean.expected.out
|
feat(frontends/lean): pp.beta is true by default
|
2015-02-24 12:27:53 -08:00 |
|
ppbug.lean
|
fix(library/print): typo in is_used_name
|
2015-01-25 08:58:08 -08:00 |
|
ppbug.lean.expected.out
|
fix(library/print): typo in is_used_name
|
2015-01-25 08:58:08 -08:00 |
|
print_ax1.lean
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
print_ax1.lean.expected.out
|
feat(frontends/lean): add 'print axioms' command, close #251
|
2014-10-24 14:35:03 -07:00 |
|
print_ax2.lean
|
feat(frontends/lean): add 'print axioms' command, close #251
|
2014-10-24 14:35:03 -07:00 |
|
print_ax2.lean.expected.out
|
fix(tests/lean/print_ax2): adjust test output
|
2015-02-24 13:34:52 -08:00 |
|
prodtst.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
prodtst.lean.expected.out
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
proj.lean
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
proj.lean.expected.out
|
fix(library/definitional/projection): remove redundant 'error in'
|
2014-10-29 16:51:06 -07:00 |
|
protected.lean
|
refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.
|
2014-09-19 15:54:32 -07:00 |
|
protected.lean.expected.out
|
feat(frontends/lean): add '[protected]' modifier
|
2014-09-03 15:01:13 -07:00 |
|
protected_test.lean
|
feat(frontends/lean): new semantics for "protected" declarations
|
2015-02-11 14:09:25 -08:00 |
|
protected_test.lean.expected.out
|
feat(frontends/lean): new semantics for "protected" declarations
|
2015-02-11 14:09:25 -08:00 |
|
pstate.lean
|
fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders
|
2014-10-26 16:11:58 -07:00 |
|
pstate.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
quasireducible.lean
|
feat(*): add [quasireducible] attribute
|
2015-03-04 22:12:49 -08:00 |
|
quasireducible.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
record_rec_protected.lean
|
fix(frontends/lean/structure_cmd): 'rec' must be marked as protected
|
2014-11-03 14:50:12 -08:00 |
|
record_rec_protected.lean.expected.out
|
fix(frontends/lean/structure_cmd): 'rec' must be marked as protected
|
2014-11-03 14:50:12 -08:00 |
|
red.lean
|
feat(frontends/lean): add '[semireducible]' attribute
|
2015-03-03 10:48:36 -08:00 |
|
red.lean.expected.out
|
feat(frontends/lean): add '[semireducible]' attribute
|
2015-03-03 10:48:36 -08:00 |
|
reserve_bugs.lean
|
fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command
|
2014-11-13 22:05:55 -08:00 |
|
reserve_bugs.lean.expected.out
|
fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command
|
2014-11-13 22:05:55 -08:00 |
|
revert_fail.lean
|
feat(library/tactic): produce better error message when a tactic fails
|
2015-02-16 18:42:15 -08:00 |
|
revert_fail.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
rewrite_fail.lean
|
feat(library/tactic): produce better error message when a tactic fails
|
2015-02-16 18:42:15 -08:00 |
|
rewrite_fail.lean.expected.out
|
feat(frontends/lean): hide subterms that do not contain metavariables
|
2015-03-13 12:42:57 -07:00 |
|
rewrite_loop.lean
|
fix(tests/lean/rewrite_loop): notation
|
2015-02-04 19:21:26 -08:00 |
|
rewrite_loop.lean.expected.out
|
feat(library/tactic/rewrite_tactic): add maximum number of iterations threshold to rewrite tactic
|
2015-02-04 16:13:15 -08:00 |
|
sec.lean
|
fix(frontends/lean/decl_cmds): do not allow section parameters/variables to shadow existing parameters/variables
|
2014-10-02 18:29:41 -07:00 |
|
sec.lean.expected.out
|
feat(frontends/lean): allow variables anywhere
|
2014-10-10 16:16:19 -07:00 |
|
sec2.lean
|
refactor(frontends/lean): add 'attribute' command
|
2015-01-24 20:23:21 -08:00 |
|
sec2.lean.expected.out
|
test(tests/lean): add new test for scoping rules
|
2015-01-22 11:41:19 -08:00 |
|
sec3.lean
|
feat(frontends/lean/parser): reject explicit universe levels in variables and parameters
|
2015-02-11 16:25:06 -08:00 |
|
sec3.lean.expected.out
|
feat(frontends/lean/parser): reject explicit universe levels in variables and parameters
|
2015-02-11 16:25:06 -08:00 |
|
shadow.lean
|
feat(frontends/lean): ML-like notation for match and recursive equations
|
2015-02-25 16:20:44 -08:00 |
|
shadow.lean.expected.out
|
feat(frontends/lean): ML-like notation for match and recursive equations
|
2015-02-25 16:20:44 -08:00 |
|
show1.lean
|
feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included
|
2014-10-22 18:11:09 -07:00 |
|
show1.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
showenv.l
|
chore(*): cleanup lean builtin symbols, replace :: with _
|
2014-01-09 08:33:52 -08:00 |
|
struct_class.lean
|
feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used
|
2014-11-03 17:47:08 -08:00 |
|
struct_class.lean.expected.out
|
fix(tests/lean/struct_class): adjust test result to reflect recent changes
|
2014-12-03 20:32:33 -08:00 |
|
t1.lean
|
refactor(kernel): rename var_decl to constant_assumption
|
2014-10-02 17:55:34 -07:00 |
|
t1.lean.expected.out
|
refactor(*): rename Bool to Prop
|
2014-07-22 09:43:18 -07:00 |
|
t2.lean
|
feat(frontends/lean/builtin_cmds): add simple 'print' command
|
2014-06-11 14:35:34 -07:00 |
|
t2.lean.expected.out
|
feat(frontends/lean/builtin_cmds): add simple 'print' command
|
2014-06-11 14:35:34 -07:00 |
|
t3.lean
|
feat(frontends/lean): allow parameters only in contexts
|
2014-10-11 17:13:56 -07:00 |
|
t3.lean.expected.out
|
feat(frontends/lean): add declaration to namespace without opening it, closes #161
|
2014-09-09 18:02:14 -07:00 |
|
t4.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
t4.lean.expected.out
|
feat(frontends/lean): change the name resolution rules: when in a namespace N that defines C, then C always refers to N.C (i.e., it overrides any alias)
|
2014-08-18 18:58:50 -07:00 |
|
t5.lean
|
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
|
2014-10-02 17:55:34 -07:00 |
|
t5.lean.expected.out
|
feat(frontends/lean): add basic pretty printer
|
2014-07-09 01:12:36 -07:00 |
|
t6.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
t6.lean.expected.out
|
feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command
|
2014-10-30 13:12:45 -07:00 |
|
t7.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
t7.lean.expected.out
|
feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command
|
2014-10-30 13:12:45 -07:00 |
|
t9.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
t9.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
t10.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
t10.lean.expected.out
|
feat(frontends/lean/pp): minimize number of spaces when pretty printing notation
|
2014-10-19 13:08:15 -07:00 |
|
t11.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
t11.lean.expected.out
|
feat(frontends/lean/pp): minimize number of spaces when pretty printing notation
|
2014-10-19 13:08:15 -07:00 |
|
t12.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
t12.lean.expected.out
|
feat(frontends/lean): add basic pretty printer
|
2014-07-09 01:12:36 -07:00 |
|
t13.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
t13.lean.expected.out
|
feat(frontends/lean): add basic pretty printer
|
2014-07-09 01:12:36 -07:00 |
|
t14.lean
|
fix(tests/lean/run): replace "open [notation]" with "open [notations]"
|
2014-12-17 18:28:38 -08:00 |
|
t14.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
tactic_var_bug.lean
|
fix(tests/lean): adjust tests to modifications to standard library
|
2014-11-30 21:16:01 -08:00 |
|
tactic_var_bug.lean.expected.out
|
fix(frontends/lean): fix pretty-printing spacing problem
|
2014-11-09 14:49:43 -08:00 |
|
test.sh
|
fix(tests/lean/nonexhaustive): remove line "warning: imported file uses 'sorry'" from test produced output
|
2015-02-01 21:25:52 -08:00 |
|
test_single.sh
|
fix(tests/lean/nonexhaustive): remove line "warning: imported file uses 'sorry'" from test produced output
|
2015-02-01 21:25:52 -08:00 |
|
test_single_pp.sh
|
chore(tests): cleanup test scripts
|
2014-06-29 09:03:39 -07:00 |
|
tuple.lean
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
tuple.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
uni_bug1.lean
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
uni_bug1.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
unifier_bug.lean
|
fix(library/unifier): broken optimization in the unifier
|
2014-10-28 16:09:41 -07:00 |
|
unifier_bug.lean.expected.out
|
fix(library/unifier): broken optimization in the unifier
|
2014-10-28 16:09:41 -07:00 |
|
unique_instances.lean
|
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
|
2015-03-13 14:47:21 -07:00 |
|
unique_instances.lean.expected.out
|
refactor(library): use [] binder annotation when declaring instances
|
2015-02-24 16:12:39 -08:00 |
|
univ.lean
|
feat(frontends/lean/elaborator): more strict test for bad universe solution
|
2014-10-02 14:29:51 -07:00 |
|
univ.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
univ_vars.lean
|
feat(frontends/lean): add 'universe variable' command
|
2014-10-11 14:22:33 -07:00 |
|
univ_vars.lean.expected.out
|
feat(kernel/level): improve universe level pretty printer
|
2014-11-14 14:51:03 -08:00 |
|
unzip_error.lean
|
feat(frontends/lean): ML-like notation for match and recursive equations
|
2015-02-25 16:20:44 -08:00 |
|
unzip_error.lean.expected.out
|
fix(tests/lean/nonexhaustive): remove line "warning: imported file uses 'sorry'" from test produced output
|
2015-02-01 21:25:52 -08:00 |
|
var.lean
|
chore(*): minimize the use of parameters
|
2014-10-09 07:13:06 -07:00 |
|
var.lean.expected.out
|
feat(frontends/lean): allow variables anywhere
|
2014-10-10 16:16:19 -07:00 |
|
var2.lean
|
chore(*): minimize the use of parameters
|
2014-10-09 07:13:06 -07:00 |
|
var2.lean.expected.out
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
|
2014-10-19 08:41:29 -07:00 |
|
varcomma.lean
|
feat(frontends/lean): better error messages for ill-terminated declarations
|
2015-02-10 14:38:00 -08:00 |
|
varcomma.lean.expected.out
|
feat(frontends/lean): better error messages for ill-terminated declarations
|
2015-02-10 14:38:00 -08:00 |
|
whnf.lean
|
test(tests/lean): remove data.nat dependency
|
2014-12-23 17:42:56 -08:00 |
|
whnf.lean.expected.out
|
fix(tests/lean/whnf): make sure the test does not produce 'sorry'
|
2014-12-03 21:12:33 -08:00 |
|
whnf_tac.lean
|
feat(library/tactic): add whnf tactic, closes #270
|
2014-10-28 23:18:49 -07:00 |
|
whnf_tac.lean.expected.out
|
feat(library/tactic): add whnf tactic, closes #270
|
2014-10-28 23:18:49 -07:00 |
