Skip to content

Commit 5f3216f

Browse files
committed
small fix
1 parent ffe12f0 commit 5f3216f

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -51,8 +51,8 @@ Type **"auto 👍"** to test whether auto is set up.
5151
* $(2)$ `duper` is unable to prove the translated problem, although the translated problem is provable
5252
* $(3)$ `auto` is unable to handle certain Lean features in the problem
5353
---
54-
To find out if the issue is caused by $(1)$, try proving the goal manually using only the basic tactics (e.g. `rw`, `apply`, `simp only`, and `dsimp only`) and the hints you provided to `lean-auto`. Try not to use `simp`, `simp_all` and `grind` because they might automatically use theorems that are not within the hint list provided to them. If you're able to prove the goal manually, it means the list of hints you provided is sufficient.
55-
To find out if the issue is caused by $(2)$, try using `lean-auto + SMT solver` and `lean-auto + TPTP solver` and see if it's able to solve the goal. Note that even if the goal is still not solved, it does not necessarily mean that the translated problem is unprovable.
54+
To find out if the issue is caused by $(1)$, try proving the goal manually using only the basic tactics (e.g. `rw`, `apply`, `simp only`, and `dsimp only`) and the hints you provided to `lean-auto`. Try not to use `simp`, `simp_all` and `grind` because they might automatically use theorems that are not within the hint list provided to them. If you're able to prove the goal manually, it means that the list of hints you provided is sufficient.
55+
To find out if the issue is caused by $(2)$, try using `lean-auto + SMT solver` and `lean-auto + TPTP solver` and see if they're able to solve the goal. Note that even if the goal is still not solved, it does not necessarily mean that the translated problem is unprovable.
5656

5757
## Utilities
5858
* Command ```#getExprAndApply [ <term> | <ident> ]```: Defined in ```ExprExtra.lean```. This command first elaborates the ```<term>``` into a lean ```Expr```, then applies function ```<ident>``` to ```Expr```. The constant ```ident``` must be already declared and be of type ```Expr → TermElabM Unit```

0 commit comments

Comments
 (0)