We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent bd81f08 commit a642840Copy full SHA for a642840
src/Lean/Meta/Tactic/ElimInfo.lean
@@ -234,7 +234,7 @@ example (x : Three) (p : Three → Prop) : p x := by
234
cases x
235
-- val : Fin 3 ⊢ p ⟨val⟩
236
237
-@[induction_eliminator, elab_as_elim]
+@[cases_eliminator, elab_as_elim]
238
def Three.myRec {motive : Three → Sort u}
239
(zero : motive ⟨0⟩) (one : motive ⟨1⟩) (two : motive ⟨2⟩) :
240
∀ x, motive x
0 commit comments