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 #224

Open
aniva wants to merge 1 commits from doc/rationale into dev
pull from: doc/rationale
merge into: aniva:dev
Conversation 0 Commits 1 Files Changed 2 +3 -7
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 $ pantograph Init
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"} goal.tactic {"stateId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"} goal.tactic {"stateId": 1, "tactic": "assumption"}
goal.delete {"stateIds": [0]} goal.delete {"stateIds": [0]}
stat {} stat {}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"} goal.tactic {"stateId": 1, "tactic": "rw [Nat.add_comm]"}
stat stat
``` ```
where the application of `assumption` should lead to a failure. 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 - 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 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. 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 Pantograph cannot perform things that are inherently constrained by Lean. These
include: include: