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.

Estimated changes