## Stream: new members

### Topic: how to unfold let?

#### 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?

#### Kevin Buzzard (Jun 10 2020 at 19:54):

Try using set instead. tactic#set

#### Kevin Buzzard (Jun 10 2020 at 19:54):

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

cool, thx

#### Bhavik Mehta (Jun 10 2020 at 20:21):

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

#### 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? :-)

#### 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.

#### Pedro Minicz (Jun 10 2020 at 22:11):

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

#### Bryan Gin-ge Chen (Jun 10 2020 at 22:12):

lean#124 is along those lines.

#### 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)

#### Mario Carneiro (Jun 10 2020 at 22:17):

there is a reason I made rintros an alias to rintro

#### Kevin Buzzard (Jun 10 2020 at 22:17):

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

#### 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

#### Mario Carneiro (Jun 10 2020 at 22:18):

they serve no useful parsing purpose

#### 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.

lol

#### Kevin Buzzard (Jun 10 2020 at 22:18):

Lean grammar police

#### Mario Carneiro (Jun 10 2020 at 22:19):

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

#### Pedro Minicz (Jun 10 2020 at 22:23):

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

#### Pedro Minicz (Jun 10 2020 at 22:23):

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

#### 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

#### 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

#### Reid Barton (Jun 11 2020 at 00:36):

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

#### Pedro Minicz (Jun 11 2020 at 00:38):

You don't necessarily need parenthesis around variables either:

variables x : ℕ
variables a b : ℕ


#### Reid Barton (Jun 11 2020 at 00:43):

Oh interesting

Last updated: May 16 2021 at 21:11 UTC