syntax in term mode

Stream: new members

[PV]

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]

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]

The second example should be

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

[Kevin Buzzard]

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

[PV]

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]

you don't get the context window either way

[Kevin Buzzard]

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]

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

[PV]

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.