Skip to content

Commit

Permalink
Update suggest_tactics figures in README
Browse files Browse the repository at this point in the history
  • Loading branch information
Peiyang-Song authored Apr 3, 2024
1 parent 839c5cf commit f206b39
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -76,11 +76,11 @@ require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "L

After `import LeanCopilot`, you can use the tactic `suggest_tactics` to generate tactic suggestions. You can click on any of the suggested tactics to use it in the proof.

<img width="977" alt="suggest_tactics" src="https://github.com/lean-dojo/LeanCopilot/assets/114432581/edb7ffbd-59b0-4112-9621-c4344ed14ac8">
<img width="977" alt="suggest_tactics" src="https://github.com/lean-dojo/LeanCopilot/assets/114432581/f06865b6-58be-4938-a75c-2a23484384b4">

You can provide a prefix (e.g., `simp`) to constrain the generated tactics:

<img width="915" alt="suggest_tactics_simp" src="https://github.com/lean-dojo/LeanCopilot/assets/114432581/ab3b75a2-e61c-4ba8-83b6-31f344f0a64d">
<img width="915" alt="suggest_tactics_simp" src="https://github.com/lean-dojo/LeanCopilot/assets/114432581/95dcae31-41cb-451c-9fdf-d73522addb6e">


#### Proof Search
Expand Down

0 comments on commit f206b39

Please sign in to comment.