# Zulip Chat Archive

## Stream: new members

### Topic: Confused about functions

#### 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 :)

#### 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