search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.55k stars 404 forks source link

`first` does not recover from `refine` type class error #1142

Closed Kha closed 2 years ago

Kha commented 2 years ago 
example : String := by
  first
  | refine toString True
  | apply "hi"

Expected behavior: The second branch should be applied without error.

Actual behavior:

failed to synthesize instance
  ToString Prop
larsk21 commented 2 years ago

This is relevant for my Iris IPM port, where I want to use a type class to parse the goal and decide, based on the form of the goal, i.e. the availability of certain type class instances, whether to use the remaining part of the theorem. At least in my case, I think refine is better suited than apply (see https://github.com/leanprover/lean4/commit/a670ed1e2d7499fb7afdd7db918b71257e89ca9f), since I have stricter control over when missing arguments are turned into goals and when the tactic will fail instead.