Zulip Chat Archive

Stream: new members

Topic: how to unfold let?


view this post on Zulip Daniel Fabian (Jun 10 2020 at 19:53):

Sometimes, I end up needing a long term maybe as part of a use. And to make things more legible, I'd introduce a term using a let binding.

example : 2 = 2 :=
begin
  let alsoTwo := 2 + 1 - 1 + 3 - 3 + 2 - 2,
  show alsoTwo = 2,
  --rw alsoTwo, -- doesn't work
  --unfold alsoTwo, -- doesn't work
end

but at this point, only refl/ simp work anymore. Any idea how I can put back the let-binding?

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 19:54):

Try using set instead. tactic#set

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 19:54):

set x := long_term with hx gives you hx that you can explicitly rewrite with.

view this post on Zulip Daniel Fabian (Jun 10 2020 at 19:56):

cool, thx

view this post on Zulip Bhavik Mehta (Jun 10 2020 at 20:21):

Is there a reason we can't make let have this with functionality too?

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 20:51):

IIRC set exists because I had the same problem as Daniel back in the days when we couldn't edit core Lean and Rob made set to stop me whining. Maybe you want to try editing core Bhavik? :-)

view this post on Zulip Pedro Minicz (Jun 10 2020 at 22:10):

I think as many quality of life improvements as possible should be made, even if it breaks a lot of stuff in the short term. This community is still small enough for this to be possible without too much of a hassle.

view this post on Zulip Pedro Minicz (Jun 10 2020 at 22:11):

Deduplicating tactics where one is a straight improvement over the other would be a great start.

view this post on Zulip Bryan Gin-ge Chen (Jun 10 2020 at 22:12):

lean#124 is along those lines.

view this post on Zulip Pedro Minicz (Jun 10 2020 at 22:12):

  • set and let
  • rintros intros (I don't even think there should be a distinction between intro and intros, its just annoying tbh)

view this post on Zulip Mario Carneiro (Jun 10 2020 at 22:17):

there is a reason I made rintros an alias to rintro

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 22:17):

Patrick I think also wants to kill intro and intros and just rename rintro to intro

view this post on Zulip Mario Carneiro (Jun 10 2020 at 22:17):

Actually I think the same can be said about all the plural command keywords: variables, axioms, parameters

view this post on Zulip Mario Carneiro (Jun 10 2020 at 22:18):

they serve no useful parsing purpose

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 22:18):

They could have made it so the plural versions don't work when there's exactly one thing following.

view this post on Zulip Mario Carneiro (Jun 10 2020 at 22:18):

lol

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 22:18):

Lean grammar police

view this post on Zulip Mario Carneiro (Jun 10 2020 at 22:19):

maybe we should use variable(s)... except that redeclares an explicit variable s

view this post on Zulip Pedro Minicz (Jun 10 2020 at 22:23):

I vote for everything being singular and working as plurals to right now.

view this post on Zulip Pedro Minicz (Jun 10 2020 at 22:23):

Also, kill intro, intros, and rintro and rename rintros to intro. :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (Jun 10 2020 at 22:24):

I think there are some dependency hurdles to moving rcases to core, but otherwise I don't think there are any blockers for this

view this post on Zulip Mario Carneiro (Jun 10 2020 at 22:25):

oh, I had planned to extend rcases patterns with type ascriptions so that obtain is a generalization

view this post on Zulip Reid Barton (Jun 11 2020 at 00:36):

Technically variable has a "purpose": you don't need parentheses around the binder

view this post on Zulip Pedro Minicz (Jun 11 2020 at 00:38):

You don't necessarily need parenthesis around variables either:

variables x : 
variables a b : 

view this post on Zulip Reid Barton (Jun 11 2020 at 00:43):

Oh interesting


Last updated: May 16 2021 at 21:11 UTC