Can i `revert` unnamed variables?

Stream: new members

[Tobias Grosser]

I happen to have come across a situation where I would like to revert unnamed variables. I prepared a contrived test case below:

theorem test : ∀ a: ℕ, 2 * a = a + a := by
  intros
  -- QUESTIONS:
  -- a) can I `revert a✝` without naming a in `intros a`?
  -- b) can I revert all `a`s of type `ℕ`, again without naming them explicitly?
  sorry

Is what I want to achieve possible?

[Eric Wieser]

revert ‹ℕ› works for your first question

[Tobias Grosser]

Amazing. Thank you @Eric Wieser

[Tobias Grosser]

Interestingly, my use case uses Option Nat instead of plain Nat. Any idea why this does not work?

theorem test : ∀ a : Option Nat, 0 = 0 := by
  intros
  revert ⟨Option Nat⟩
  -- QUESTION:
  -- why does this not work?
  sorry
-- invalid constructor ⟨...⟩, expected type must be an inductive type
--  ?m.128390

Option is clearly an inductive type:

inductive Option (α : Type u) where
  /-- No value. -/
  | none : Option α
  /-- Some value of type `α`. -/
  | some (val : α) : Option α

[Eric Wieser]

Those are not the same angle brackets

[Tobias Grosser]

Now it works like a charm.

[Tobias Grosser]

Thank you.