Zulip Chat Archive

Stream: new members

Topic: Return a value where the type depends on input values?


view this post on Zulip Nicholas Dyson (Oct 28 2020 at 11:59):

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!

view this post on Zulip Julian Berman (Oct 28 2020 at 12:04):

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

view this post on Zulip Nicholas Dyson (Oct 28 2020 at 12:17):

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!

view this post on Zulip Eric Wieser (Oct 28 2020 at 12:50):

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


Last updated: May 18 2021 at 17:44 UTC