| .. |
|
1313.lean
|
|
|
|
1313.lean.expected.out
|
|
|
|
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
|
|
|
|
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
|
|
|
|
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
|
|
|
|
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
|
|
|
|
focus.lean.expected.out
|
|
|
|
goal_info.lean
|
|
|
|
goal_info.lean.expected.out
|
|
|
|
goal_info_rw.lean
|
|
|
|
goal_info_rw.lean.expected.out
|
|
|
|
info.lean
|
|
|
|
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
|
|
|
|
info_id_pre_elab.lean
|
|
|
|
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
|
|
|
|
nested_traces.lean
|
|
|
|
nested_traces.lean.expected.out
|
|
|
|
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
|
|
|
|
run_single.sh
|
|
|
|
sync.input
|
|
|
|
sync.input.expected.out
|
|
|
|
test_single.sh
|
|
|
|
trace.lean
|
|
|
|
trace.lean.expected.out
|
|
|
