let expression with typing statement?

Stream: new members

[Chris M]

In the following:

lemma qimpE (T:Type*) (P:T → Prop) [h:FinT T] [h:∀t, decidable (P t)] :
    zero < (sumpred P (count T)) → ∃t:T, P t :=
assume assum, let ⟨c, h⟩ := deflt assum in

It would be helpful to add type annotations to c and h, and write \< c:nat, h:a+c=b\>. Apparently, this gives an error:

invalid constructor, `⟩` expected
main.lean:40:20
don't know how to synthesize placeholder
context:
T : Type u_1,
P : T → Prop,
h : FinT T,
h : Π (t : T), decidable (P t),
assum : 0 < sumpred P (count T)
⊢ Sort ?

Is there a way to fix this?

[Reid Barton]

The obtain tactic supports this syntax

[Reid Barton]

e.g.

begin
  intro assum,
  obtain \< c:nat, h:a+c=b\> := deflt assum,
  ...
end

[Reid Barton]

It's part of the rcases pattern language

[Mario Carneiro]

rcases is basically strictly better than lean's built in destructuring lam/let at this point