Return a value where the type depends on input values?

Stream: new members

[Nicholas Dyson]

Hello there. I've been learning Lean and there's something that I want to do that I think should be possible but I have no idea how to write it. The following example is as minimal as I can make it:
Suppose I have a type foo and then a dependent type

inductive dependent (a : foo) : Type
| baz : dependent

And then I want to make a function func that takes a value bar of type foo as an argument and returns a value of type (dependent bar). Basically, the return type of the function needs to partially depend on the value of the argument. The Lean manual suggests that this is possible, but I couldn't actually see any examples of how to write it. My reading of the manual leads me to think (and I may well be wrong) the syntax for the type declaration is

def func : foo -> Π {k : foo}, (dependent k)

but I have no idea what then goes in the actual definition.

Thanks for any help!

[Julian Berman]

Is this what you're after?

inductive foo
| FOO
| BAR

inductive dependent (a : foo) : Type
| baz : dependent

def func (f : foo) : dependent f := dependent.baz

[Nicholas Dyson]

YES, thank you so much; that does what I want and now that I know what it's supposed to look like I've been able to make the actual version do what I want. You're a star!

[Eric Wieser]

I think structure dependent (a : foo) would work just fine in that example