| .. |
|
config.lean
|
feat(tests/lean/interactive): add interactive mode test script
|
2013-12-05 16:56:20 -08:00 |
|
config.lean.expected.out
|
feat(tests/lean/interactive): add interactive mode test script
|
2013-12-05 16:56:20 -08:00 |
|
t1.lean
|
feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
|
2013-12-05 20:06:32 -08:00 |
|
t1.lean.expected.out
|
feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'
|
2013-12-06 14:49:39 -08:00 |
|
t2.lean
|
feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
|
2013-12-05 20:06:32 -08:00 |
|
t2.lean.expected.out
|
feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'
|
2013-12-06 14:49:39 -08:00 |
|
t3.lean
|
feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
|
2013-12-05 20:06:32 -08:00 |
|
t3.lean.expected.out
|
test(tests/lean/interactive): add back command test
|
2013-12-05 17:19:53 -08:00 |
|
t4.lean
|
fix(frontends/lean/parser): remove unnecessary '#' after error
|
2013-12-05 17:27:08 -08:00 |
|
t4.lean.expected.out
|
fix(frontends/lean/parser): remove unnecessary '#' after error
|
2013-12-05 17:27:08 -08:00 |
|
t5.lean
|
feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
|
2013-12-05 20:06:32 -08:00 |
|
t5.lean.expected.out
|
fix(frontends/lean/parser): bug in parse_tactic
|
2013-12-05 17:40:55 -08:00 |
|
t6.lean
|
feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
|
2013-12-05 20:06:32 -08:00 |
|
t6.lean.expected.out
|
feat(frontends/lean/parser): allow the user to use a theorem/axiom name as an argument for the apply tactic command
|
2013-12-05 19:03:12 -08:00 |
|
t7.lean
|
feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command
|
2013-12-05 20:08:51 -08:00 |
|
t7.lean.expected.out
|
feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command
|
2013-12-05 20:08:51 -08:00 |
|
t8.lean
|
feat(library/tactic/proof_state): add option tactic::proof_state::goal_names
|
2013-12-05 21:18:22 -08:00 |
|
t8.lean.expected.out
|
feat(library/tactic/proof_state): add option tactic::proof_state::goal_names
|
2013-12-05 21:18:22 -08:00 |
|
t9.lean
|
fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found
|
2013-12-06 05:13:29 -08:00 |
|
t9.lean.expected.out
|
fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found
|
2013-12-06 05:13:29 -08:00 |
|
t10.lean
|
fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found
|
2013-12-06 05:13:29 -08:00 |
|
t10.lean.expected.out
|
feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'
|
2013-12-06 14:49:39 -08:00 |
|
t11.lean
|
fix(frontends/lean/notation): change the precedence of '->'
|
2013-12-06 13:23:24 -08:00 |
|
t11.lean.expected.out
|
fix(frontends/lean/notation): change the precedence of '->'
|
2013-12-06 13:23:24 -08:00 |
|
t12.lean
|
feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms
|
2013-12-06 15:01:54 -08:00 |
|
t12.lean.expected.out
|
feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms
|
2013-12-06 15:01:54 -08:00 |
|
test.sh
|
feat(tests/lean/interactive): add interactive mode test script
|
2013-12-05 16:56:20 -08:00 |
|
test_single.sh
|
feat(tests/lean/interactive): add interactive mode test script
|
2013-12-05 16:56:20 -08:00 |
