| .. |
|
1313.lean
|
test(tests/lean/interactive): add regression test for #1313
|
2017-01-20 21:48:19 -08:00 |
|
1313.lean.expected.out
|
chore(tests): changed sorry warnings
|
2017-03-23 08:57:56 +01:00 |
|
complete.lean
|
feat(frontends/lean/{builtin_cmds,interactive}): complete namespace/section after end
|
2017-04-23 11:26:31 -07:00 |
|
complete.lean.expected.out
|
feat(frontends/lean/{builtin_cmds,interactive}): complete namespace/section after end
|
2017-04-23 11:26:31 -07:00 |
|
complete_field.lean
|
feat(frontends/lean,shell): autocompletion for ^.
|
2017-01-17 19:27:59 -08:00 |
|
complete_field.lean.expected.out
|
chore(*): replace "'^.' notation" with "field notation", pretty print using "."
|
2017-03-31 09:40:49 -07:00 |
|
complete_import.lean
|
feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes
|
2017-01-10 12:25:33 +01:00 |
|
complete_import.lean.expected.out
|
fix(library/module_mgr): do not crash on missing imports
|
2017-04-04 19:56:33 +02:00 |
|
complete_namespace.lean
|
fix(frontends/lean/builtin_cmds): do not complete after namespace
|
2017-01-10 14:42:48 -08:00 |
|
complete_namespace.lean.expected.out
|
fix(frontends/lean/builtin_cmds): do not complete after namespace
|
2017-01-10 14:42:48 -08:00 |
|
complete_scanner_error.lean
|
fix(frontends/lean/parser): catch exceptions thrown by sync_command
|
2017-01-10 14:42:48 -08:00 |
|
complete_scanner_error.lean.expected.out
|
chore(tests): changed sorry warnings
|
2017-03-23 08:57:56 +01:00 |
|
complete_tactic.lean
|
feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes
|
2017-01-10 12:25:33 +01:00 |
|
complete_tactic.lean.expected.out
|
chore(tests): changed sorry warnings
|
2017-03-23 08:57:56 +01:00 |
|
complete_trailing_period.lean
|
|
|
|
complete_trailing_period.lean.expected.out
|
chore(tests/lean): fix tests
|
2017-03-15 19:40:52 -07:00 |
|
correct_snapshot_invalidation.input
|
fix(frontends/lean/scanner): correctly handle positions in empty files
|
2017-03-31 09:40:15 -07:00 |
|
correct_snapshot_invalidation.input.expected.out
|
fix(frontends/lean/scanner): correctly handle positions in empty files
|
2017-03-31 09:40:15 -07:00 |
|
do_info.lean
|
fix(frontends/lean): auxiliary bind-application in do-notation was not allowing us to obtain type information for the monadic actions.
|
2017-01-12 18:38:31 -08:00 |
|
do_info.lean.expected.out
|
chore(*): fix tests
|
2017-03-23 09:03:43 +01:00 |
|
field_info.lean
|
fix(frontends/lean/interactive): fix info on new field notation
|
2017-03-31 09:40:49 -07:00 |
|
field_info.lean.expected.out
|
feat(frontends/lean/builtin_exprs): use local field inference for info too
|
2017-03-27 14:01:38 -07:00 |
|
focus.lean
|
fix(frontends/lean/{interactive,tactic_notation}): fix tests
|
2017-03-17 18:20:44 -07:00 |
|
focus.lean.expected.out
|
refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic
|
2017-03-23 09:07:08 +01:00 |
|
goal_info.lean
|
fix(frontends/lean/{interactive,tactic_notation}): fix tests
|
2017-03-17 18:20:44 -07:00 |
|
goal_info.lean.expected.out
|
fix(frontends/lean/tactic_notation): add skip tactic to save intermediate result
|
2017-01-20 20:58:05 -08:00 |
|
goal_info_rw.lean
|
feat(init/meta/interactive): rw goal info on ]
|
2017-03-22 07:54:12 -07:00 |
|
goal_info_rw.lean.expected.out
|
refactor(init/meta/interactive): rw: parse - separately to remove hack
|
2017-03-22 07:54:12 -07:00 |
|
info.lean
|
chore(frontends/lean): rename transient commands
|
2017-03-09 18:41:19 -08:00 |
|
info.lean.expected.out
|
chore(*): fix tests
|
2017-03-23 09:00:59 +01:00 |
|
info1.lean
|
|
|
|
info1.lean.expected.out
|
chore(test/lean/interactive): do not test for exact source information
|
2017-02-17 13:45:56 +01:00 |
|
info_goal.lean
|
fix(frontends/lean/tactic_notation): report state after tactic execution on ,
|
2017-01-17 16:38:00 -08:00 |
|
info_goal.lean.expected.out
|
fix(frontends/lean/{interactive,tactic_notation}): fix tests
|
2017-03-17 18:20:44 -07:00 |
|
info_id_pre_elab.lean
|
feat(frontends/lean/parser): save id info for non-overloaded constants
|
2017-03-22 07:35:14 -07:00 |
|
info_id_pre_elab.lean.expected.out
|
chore(tests/lean/interactive): fix test
|
2017-03-23 09:14:32 +01:00 |
|
info_tactic.lean
|
fix(frontends/lean/interactive): fall back to elaborator info when not an interactive tactic
|
2017-04-23 11:26:31 -07:00 |
|
info_tactic.lean.expected.out
|
fix(frontends/lean/interactive): fall back to elaborator info when not an interactive tactic
|
2017-04-23 11:26:31 -07:00 |
|
mk_input.sh
|
feat(frontends/lean,library/scoped_ext,shell): complete namespaces
|
2017-01-10 12:25:33 +01:00 |
|
my_tac_class.lean
|
refactor(init/meta/interaction_monad): replace rstep by istep
|
2017-03-23 09:03:41 +01:00 |
|
my_tac_class.lean.expected.out
|
refactor(init/meta/interaction_monad): replace rstep by istep
|
2017-03-23 09:03:41 +01:00 |
|
nested_traces.lean
|
fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place
|
2017-02-05 18:20:10 -08:00 |
|
nested_traces.lean.expected.out
|
chore(tests): changed sorry warnings
|
2017-03-23 08:57:56 +01:00 |
|
rb_map_ts.lean
|
refactor(init/meta/interaction_monad): replace rstep by istep
|
2017-03-23 09:03:41 +01:00 |
|
rb_map_ts.lean.expected.out
|
refactor(init/meta/interaction_monad): replace rstep by istep
|
2017-03-23 09:03:41 +01:00 |
|
run_single.sh
|
fix(test/lean/interactive/run_single): include stderr
|
2017-03-17 18:05:19 -07:00 |
|
sync.input
|
|
|
|
sync.input.expected.out
|
|
|
|
test_single.sh
|
feat(interactive/test_single): colorized diff
|
2017-02-06 15:08:45 +01:00 |
|
trace.lean
|
fix(library/init/meta): bug introduced 9bee8ce36d
|
2017-02-03 17:01:46 -08:00 |
|
trace.lean.expected.out
|
chore(tests): changed sorry warnings
|
2017-03-23 08:57:56 +01:00 |
