Skip to content

[Bug] [Lean] Clicking suggestions in Verbose Lean does not propagate the change #331

@pimotte

Description

@pimotte

Verbose Lean has a mechanism to provide suggestions through shift+clicking parts of goals and hypotheses. This works, but clicking the suggestion does not implement it.

Reproduction:

  1. Checkout https://github.com/impermeable/waterproof-exercises-lean/tree/c0932711ab104a5fa73367055f8facf3b6ebab4a
  2. Add "useDefaultSuggestionProviders" on a single line, after the imports, before #doc in WaterproofExercisesLean/example_file.lean
  3. Move your cursor to the start of the input area of exercise 1.1.14
  4. Shift+Click the middle "\and" symbol in the goal in the tactic state (not in the "We need to show")
  5. Observe the suggestions: Let's first prove that p ∧ q and Let's first prove that r ∧ s
  6. Click either. It will not be inserted, and it should be.

Metadata

Metadata

Assignees

Labels

bugSomething isn't working

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions