550fa6994e
right now, the `induction` tactic accepts a custom eliminator using the `using <ident>` syntax, but is restricted to identifiers. This limitation becomes annoying when the elminator has explicit parameters that are not targets, and the user (naturally) wants to be able to write ``` induction a, b, c using foo (x := …) ``` This generalizes the syntax to expressions and changes the code accordingly. This can be used to instantiate a multi-motive induction: ``` example (a : A) : True := by induction a using A.rec (motive_2 := fun b => True) case mkA b IH => exact trivial case A => exact trivial case mkB b IH => exact trivial ``` For this to work the term elaborator learned the `heedElabAsElim` flag, `true` by default. But in the default setting, `A.rec (motive_2 := fun b => True)` would fail to elaborate, because there is no expected type. So the induction tactic will elaborate in a mode where that attribute is simply ignored. As a side effect, the “failed to infer implicit target” error message is improved and prints the name of the implicit target that could not be instantiated.
0 lines
Text
0 lines
Text