Commit 2021-10-14 07:32 ade323e3
View on Github →feat(Tactic/ShowTerm): port of show_term (#44)
showTerm
wraps another tactic, and prints a "Try this: ..." message containing a term that contain replace the tactic invocation.
In future, we will implement code actions in the editor rather that expect the editor to parse this trace message string.