aeneas icon indicating copy to clipboard operation
aeneas copied to clipboard

Published 20 hours ago • verified publisher icon AeneasVerif

`progres*?` shows Aesop's add this message.

Open ayhon opened this issue 8 months ago • 0 comments

Since we're currently using Aesop's addTryThisTacticSeqSuggestion function, the prompt makes it seem like the suggestion is coming from the Aesop tactic.

https://github.com/AeneasVerif/aeneas/blob/0c87ae52b7963acabb8d487bd55e573ff56a94f6/backends/lean/Aeneas/Progress/ProgressStar.lean#L365-L369

Image

ayhon avatar Mar 27 '25 22:03 ayhon