lean4-htt/tests/lean/interactive
2017-01-10 12:25:33 +01:00
..
complete.lean feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes 2017-01-10 12:25:33 +01:00
complete.lean.expected.out feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes 2017-01-10 12:25:33 +01: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 feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes 2017-01-10 12:25:33 +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 feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes 2017-01-10 12:25:33 +01:00
complete_trailing_period.lean chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
complete_trailing_period.lean.expected.out chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
field_info.lean chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
field_info.lean.expected.out chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
info.lean chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
info.lean.expected.out chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
info1.lean chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
info1.lean.expected.out chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
info_goal.lean feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes 2017-01-10 12:25:33 +01:00
info_goal.lean.expected.out feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes 2017-01-10 12:25:33 +01:00
info_notation.lean chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
info_notation.lean.expected.out chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
info_notation1.lean chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
info_notation1.lean.expected.out chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
mk_input.sh chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
run_single.sh chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
sync.input chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
sync.input.expected.out chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00
test_single.sh chore(tests/lean/interactive): simplify input format and test full completion output 2017-01-10 12:25:33 +01:00