Zulip Chat Archive

Stream: general

Topic: clear after rintro/rcases


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Aug 19 2020 at 18:33):

How about !?

view this post on Zulip Simon Hudon (Aug 19 2020 at 18:34):

Or \?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:18):

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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 20:18):

How about -?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 22:05):

#3868

view this post on Zulip Simon Hudon (Aug 19 2020 at 22:38):

Is it maybe too similar to _?

view this post on Zulip 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

view this post on Zulip Simon Hudon (Aug 19 2020 at 23:48):

I think we can worry about both at once

view this post on Zulip 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).

view this post on Zulip Johan Commelin (Aug 20 2020 at 02:50):

@Mario Carneiro Thanks for the PR!


Last updated: May 08 2021 at 19:11 UTC