aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 4 Packages Projects Releases Wiki Activity

doc: Remove constraint on pick_goal

This commit is contained in:
Leni Aniva 2025-06-30 15:56:48 -07:00
parent f26b7fc177
commit 50bb48f2ed
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
2 changed files with 3 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
README.md
View File

@ -60,11 +60,11 @@ Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_
```
$ pantograph Init
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
goal.tactic {"stateId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "tactic": "assumption"}
goal.delete {"stateIds": [0]}
stat {}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
goal.tactic {"stateId": 1, "tactic": "rw [Nat.add_comm]"}
stat
```
where the application of `assumption` should lead to a failure.

4
doc/rationale.md
View File

@ -37,10 +37,6 @@ differently from Lean in some times, but never at the sacrifice of soundness.
- When Lean LSP says "unresolved goals", that means a proof cannot finish where
it is supposed to finish at the end of a `by` block. Pantograph will raise the
error in this case, since it indicates the termination of a proof search branch.
- `pick_goal` or `swap` will not work since they run contrary to tree search
paradigms. However, if there are tactics which perform non-trivial operations
to multiple goals at the same time, this constrain could potentially be
relaxed at a cost of great bookkeeping overhead to the user.
Pantograph cannot perform things that are inherently constrained by Lean. These
include: