## Stream: new members

#### Pehan Amarathunge (Jan 26 2023 at 18:25):

Hi there.

I have just started learning Lean and I am confused about how functions work.

I was able to solve the below example in a sequence of steps, but I don't understand why the following code does not solve the same problem in one line. I would really appreciate some sort of help on this.

Thank you :)

image.png

#### Gareth Ma (Jan 26 2023 at 18:35):

Hey, next time post the code directly instead, enclosed using \\\, so that people can copy and paste :) Anyways, try this:

example {A B C D : Type} (f : A → B → C → D) (g : A → B) (x : A) (z : C) : D :=
begin
exact f x (g x) z, -- g x = g(x)
end


#### Gareth Ma (Jan 26 2023 at 18:38):

The problem can be seen if you run your code and look at the error:

function expected at
x
term has type
A


which occurs in your parentheses (x g(x) z). It is because if you put parentheses around them, it will treat it as a single expression and try to compute/evaluate it. And since you wrote x _ _, it only makes sense if x is a function, but it is not - it is just a type A

#### Gareth Ma (Jan 26 2023 at 18:40):

If you remove the parentheses like I did, this is what happens:

f         -- Type: A -> B -> C -> D
x       -- We evaluate the above line at x. Now (f x) has type B -> C -> D
(g x) -- We evaluate the above line at (g x). (g x) = g(x) has type B,
-- so (f x g(x)) has type C -> D
z   -- Finish it


#### Gareth Ma (Jan 26 2023 at 18:42):

Oh also if you write f x g(x) z it will be interpreted as (f x g)(x) z.

#### Junyan Xu (Jan 26 2023 at 23:42):

f (x g(x) z) is the same as f (x g x z)` I think ...

Last updated: Dec 20 2023 at 11:08 UTC