name function without function body

Stream: Is there code for X?

[Robert Osazuwa Ness]

Beginner question. I'm working through a functional programming book I like and trying to learn by converting haskell and scala code to lean. I'm trying to reason about function composition. In haskell you can write functions g and f and compose them as follows.

f :: A -> B
g :: B -> C
g . f

In haskell, you can write as follows:

val f: A => B
val g: B => C
g compose f

I know in Lean there is a composition shorthand g ∘ f . But is there a way of naming a function and it's type (A->B) without providing a function body in lean? Something like:

def f: A → B
def g: B → C
g ∘ f

But this code isn't valid because the first two lines need a ":=" and a function body.

[Damiano Testa]

Does

variables (f : A → B) (g : B → C)
#check g ∘ f

work?

[Robert Osazuwa Ness]

Thanks @Damiano Testa that helps!

[Matt Diamond]

might be worth noting that one other way to do this is to simply declare the functions as constants, like:

constant f : A → B
constant g : B → C

[Matt Diamond]

on second thought, that's probably the wrong way to go about it... it looks like #check g ∘ f has metavariables rather than the expected types