curly begin end blocks

Stream: general

[Mario Carneiro]

Here's a lean grammar fact I just learned while reading the code: { tacs } can be used to start a tactic block without by or begin after have and show:

example := show 1 + 1 = 2, { exact rfl }
example := have 1 + 1 = 2, { exact rfl }, trivial

[Gihan Marasingha]

Awesome! I'll never use begin again.

import data.vector

def myseq : Π (k : ℕ), vector ℕ k → vector ℕ (k+1) :=
show Π (k : ℕ), vector ℕ k → vector ℕ (k+1),
{ intro k,
  refine nat.rec_on k _ _,
  { intro am, exact ⟨[1], rfl⟩, },
  { intros m h am,
    refine nat.rec_on m _ _,
    { exact ⟨[1, 1], rfl⟩ },
    { intros c ac, exact vector.cons (ac.head + ac.tail.head) ac }, }, }