feat: A-star search #3973
feat: A-star search #3973
Conversation
|
Eventually this is leading to a reimplementation of the original |
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
bors
bot
changed the base branch from
master
to
ScottCarnahan/BinomialRing2
semorrison
changed the base branch from
ScottCarnahan/BinomialRing2
to
master
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| heuristicPrio := default | ||
| totalPrio := default | ||
| explored := [] | ||
| remaining := .nil }⟩ |
There was a problem hiding this comment.
Maybe just write deriving Inhabited after Path and VertexData instead of doing this manually?
| recursively record all paths obtained by adding a previously explored edge to this path. | ||
| -/ | ||
| partial def recordPath (Γ : GraphData m P V E) (optimal : Bool) (path : Path P V E) : | ||
| (M m P V E) PUnit := do |
There was a problem hiding this comment.
| (M m P V E) PUnit := do | |
| M m P V E PUnit := do |
| /-- The best so far path to the vertex. -/ | ||
| bestPath : Path P V E | ||
| /-- The heuristic associated to the vertex. -/ | ||
| heuristicPrio : P |
There was a problem hiding this comment.
Is there a reason to track this here, because it's always the same as Γ.heuristic v for the v this is associated to, right? The single occurrence of d.heuristicPrio below can become Γ.heuristic v.
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
the
merge-conflict
|
This was support for a previously planned implementation of |
This is intended for meta programming, not proving.