Zulip Chat Archive

Stream: new members

Topic: let expression with typing statement?


view this post on Zulip Chris M (Nov 03 2020 at 17:02):

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?

view this post on Zulip Reid Barton (Nov 03 2020 at 17:17):

The obtain tactic supports this syntax

view this post on Zulip Reid Barton (Nov 03 2020 at 17:17):

e.g.

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

view this post on Zulip Reid Barton (Nov 03 2020 at 17:18):

It's part of the rcases pattern language

view this post on Zulip Mario Carneiro (Nov 03 2020 at 18:20):

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


Last updated: May 14 2021 at 06:16 UTC