Zulip Chat Archive

Stream: new members

Topic: syntax in term mode


PV (Apr 15 2020 at 15:53):

All, had a question on syntax as I'm still trying to get more comfortable with term mode. From an example in TPIL I was trying to match the "have" and "from" terms when the corresponding lambdas:

variables (p q : Prop)

example (hpp : p) (h : p  q) : q :=
have hp : p, from and.left h, _

example (hpp : p) (h : p  q) : q :=
(λ (hp : p), and.left h) _

The goal window shows a different result in both cases.

Kevin Buzzard (Apr 15 2020 at 15:58):

If you put ```lean at the top then you get syntax highlighting. If you put variables (p q : Prop) then your code compiles as it stands so people can just cut and paste it. The second example is a type mismatch so your question is difficult to make sense of.

Reid Barton (Apr 15 2020 at 15:59):

The second example should be

example (hpp : p) (h : p  q) : q :=
(λ (hp : p), _) (and.left h)

Kevin Buzzard (Apr 15 2020 at 15:59):

In the first example, the have means "put the goal on hold, I'm adding another proof to the local context"

PV (Apr 15 2020 at 16:08):

Thanks, so is it just a disadvantage that you don't get the same context window when trying to use the lambda syntax and skipping the have and from?

Mario Carneiro (Apr 15 2020 at 16:10):

you don't get the context window either way

Kevin Buzzard (Apr 15 2020 at 16:10):

variables (p q : Prop)

example (hpp : p) (h : p  q) : q :=
(λ (hp : p), (_ : q)) (and.left h)

gives the same as the first example

Mario Carneiro (Apr 15 2020 at 16:10):

The advantage of have is simply that it reads more naturally and is easier to format

PV (Apr 15 2020 at 16:12):

Kevin Buzzard said:

variables (p q : Prop)

example (hpp : p) (h : p  q) : q :=
(λ (hp : p), (_ : q)) (and.left h)

gives the same as the first example

Ahh, ok so giving it the ": q" shows the context window as the have and from example. Thanks. Sorry that is what I meant by the context windows matching between the two.


Last updated: Dec 20 2023 at 11:08 UTC