max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/interactive
History
Leonardo de Moura ca5439c698 feat(frontends/lean/tactic_notation): add support for tac ; [tac_1, ..., tac_n] notation in interactive tactic mode 
closes #1634

This commit also changes the semantic of `tactic.focus [tac_1, ..., tac_n]`.
It now fails if the number of goals is not `n`.
Before it would only fail if there were more tactics than goals.

@Armael: See tests/lean/run/handthen.lean for examples of the new notation.
2017-06-02 11:38:04 -07:00
..
1313.lean
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
complete_field.lean.expected.out chore(tests/lean/interactive/complete_field): fix test 2017-05-27 10:18:44 -07:00
complete_import.lean
complete_import.lean.expected.out fix(frontends/lean/parser): show exception message in import errors 2017-04-27 16:04:18 -07:00
complete_namespace.lean
complete_namespace.lean.expected.out
complete_scanner_error.lean
complete_scanner_error.lean.expected.out chore(tests): changed sorry warnings 2017-03-23 08:57:56 +01:00
complete_tactic.lean
complete_tactic.lean.expected.out feat(library/compiler/eta_expansion): also eta-expand expressions containing sorry 2017-05-23 11:14:31 -07: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 chore(tests): update tests with changes to error recovery 2017-05-23 11:14:30 -07:00
do_info.lean
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 fix(frontends/lean/elaborator): do not leak _elab_u names 2017-05-23 11:14:31 -07:00
focus.lean fix(frontends/lean/{interactive,tactic_notation}): fix tests 2017-03-17 18:20:44 -07:00
focus.lean.expected.out feat(frontends/lean/tactic_notation): add support for tac ; [tac_1, ..., tac_n] notation in interactive tactic mode 2017-06-02 11:38:04 -07: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
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 refactor(library): avoid auxiliary definitions such as add/mul/le/etc 2017-05-01 08:52:19 -07:00
info1.lean
info1.lean.expected.out
info_goal.lean
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 fix(frontends/lean/builtin_cmds): suppress unhelpful #check output 2017-05-23 11:14:31 -07: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 refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields 2017-04-24 19:35:15 +02:00
mk_input.sh
my_tac_class.lean fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks 2017-05-23 07:28:34 +02: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
nested_traces.lean.expected.out chore(tests): changed sorry warnings 2017-03-23 08:57:56 +01:00
rb_map_ts.lean fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks 2017-05-23 07:28:34 +02: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
trace.lean
trace.lean.expected.out chore(tests): changed sorry warnings 2017-03-23 08:57:56 +01:00