Zulip Chat Archive

Stream: new members

Topic: syntax question about lambda


Marcus Rossel (Nov 29 2021 at 09:12):

Yes, Lean uses the syntax λ x : α, <expression using x> to denote a function that maps all x (of type α in this case) to some value that can depend on x.
Assuming f to be a function of type α -> α, the expression f (f x) will also be of type α. So your entire lambda expression ends up being a function of type α -> α.


Last updated: Dec 20 2023 at 11:08 UTC