aeneas
aeneas copied to clipboard
`progres*?` shows Aesop's add this message.
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