how to unfold let?

Stream: new members

[Daniel Fabian]

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]

Try using set instead. tactic#set

[Kevin Buzzard]

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

[Daniel Fabian]

cool, thx

[Bhavik Mehta]

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

[Kevin Buzzard]

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]

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]

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

[Bryan Gin-ge Chen]

lean#124 is along those lines.

[Pedro Minicz]

• 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]

there is a reason I made rintros an alias to rintro

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

they serve no useful parsing purpose

[Kevin Buzzard]

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

[Mario Carneiro]

lol

[Kevin Buzzard]

Lean grammar police

[Mario Carneiro]

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

[Pedro Minicz]

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

[Pedro Minicz]

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

[Mario Carneiro]

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]

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

[Reid Barton]

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

[Pedro Minicz]

You don't necessarily need parenthesis around variables either:

variables x : ℕ
variables a b : ℕ

[Reid Barton]

Oh interesting