## Stream: general

### Topic: clear after rintro/rcases

#### Johan Commelin (Aug 19 2020 at 09:49):

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 (Aug 19 2020 at 09:53):

For univ you could use ⟨⟩:

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


#### Floris van Doorn (Aug 19 2020 at 17:30):

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 (Aug 19 2020 at 18:33):

How about !?

#### Simon Hudon (Aug 19 2020 at 18:34):

Or \?

#### Mario Carneiro (Aug 19 2020 at 20:18):

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

#### Mario Carneiro (Aug 19 2020 at 20:18):

How about -?

#3868

#### Simon Hudon (Aug 19 2020 at 22:38):

Is it maybe too similar to _?

#### Mario Carneiro (Aug 19 2020 at 22:40):

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 (Aug 19 2020 at 23:48):

I think we can worry about both at once

#### Mario Carneiro (Aug 20 2020 at 00:09):

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 (Aug 20 2020 at 02:50):

@Mario Carneiro Thanks for the PR!

Last updated: May 08 2021 at 19:11 UTC