unable to create new function

Stream: new members

[abaaba]

have test: ℕ -> ℝ := λ(x:ℕ) ((1 / (x + 1)):ℝ), fails with invalid binder, identifier expected

[Bryan Gin-ge Chen]

You want something more like:

have test: ℕ -> ℝ := λ(x:ℕ), ((1 / (x + 1)):ℝ),

Note the extra comma.

[abaaba]

thanks! btw can I write in def grammar, where parameters appear at left hand side of equal sign?

[Bryan Gin-ge Chen]

You probably want to use let rather than have with this though. have will forget the definition and only keep the type.

[Bryan Gin-ge Chen]

Sorry, I don't know what you mean by "def grammar".

[Eric Wieser]

I think that's a request for:

have test (n : ℕ) : ℝ := ((1 / (x + 1)):ℝ),

to be valid syntax, which I agree is appealing

[Mario Carneiro]

let already supports it in term mode

[Eric Wieser]

I had no idea