clear after rintro/rcases

Stream: general

[Johan Commelin]

Sometimes you get hypotheses like x \in univ...
I don't like it when they clutter up the goal state, but writing clear hx everytime is also not nice.
How about, if rintro sees the pattern __ (double underscore), then it just drops that hypothesis?

[Gabriel Ebner]

For univ you could use ⟨⟩:

example : ∀ x ∈ (set.univ : set ℕ), x = x :=
begin
  rintros x ⟨⟩,
/-
x : ℕ
⊢ x = x
-/
  refl,
end

[Floris van Doorn]

I would also like if rintro has a way of just removing a hypothesis. Coq uses _ for "delete this hypothesis" and ? for our _ (choose the name of the hypothesis automatically).

[Mario Carneiro]

How about !?

[Simon Hudon]

Or \?

[Mario Carneiro]

\ is the leader key so it's not nice to type

[Mario Carneiro]

How about -?

[Mario Carneiro]

#3868

[Simon Hudon]

Is it maybe too similar to _?

[Mario Carneiro]

I think we should handle the difference between | and ∣ before we have any ground to stand on as far as that is concerned

[Simon Hudon]

I think we can worry about both at once

[Mario Carneiro]

we can keep the straw poll open some more, but personally I think the answer to "is it too similar" is no. it's quite visibly different, particularly with bracketing operators around it. (Also the original __ suggestion is even worse by this metric.) The only argument I can see re: similarity is if people forget which thing means what, but I really think that having a short way to do this is helpful. I know I will use this all the time (I remarked on it in the new members stream when it came up less than an hour after the PR).

[Johan Commelin]

@Mario Carneiro Thanks for the PR!