Skip to content

Add relevant tactic snippets to help output #247

@raulTUe

Description

@raulTUe

Comes as a result of issue #198. The help button currently returns a message saying "hint: replace with ". The goal is to add any relevant tactics along with a button to copy/insert it into the input area.

For instance, an snippet of the help output currently is:
"The goal is to show a 'there exists'-statement (∃). Choose a specific variable in ℝ.
Hint, replace with: Choose ... := ...."

Here, tactics that begin with the keyword Choose could be placed below this text, e.g:
"The goal is to show a 'there exists'-statement (∃). Choose a specific variable in ℝ.
Hint, replace with: Choose ... := ....
Tactics:
Choose (name_var) := (expression)."

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions