Zulip Chat Archive

Stream: new members

Topic: Nested Inductive Type Resolution with Match Syntax Issue


Andrew Elsey (Jun 16 2021 at 16:02):

Hi, essentially I have a nested inductive type with several type parameters. In the picture below, it is the prod case. The prod case has two nested arguments which determine the type parameters of the constructed term. The problem is when I go to write any function which matches on the constructors. I can't even write the case for the nested constructor without getting a type resolution error. To be more explicit, the function expects the matched value to be (fm K dim id_vec), but it's claiming the prod constructor stores a value of (fm K (dim1 + dim2) (add_maps id1 id2), where ideally I'd like Lean simply to figure out that (dim1 + dim2 = dim). Is there any way I can provide a proof of this or any attribute I'm unaware of? Anyone run into any similar problems? Note: I can, as shown in the second picture, use tactic mode to write function bodies instead of matching, so something works, but, unfortunately, I do need the match syntax for the recursion. Thank you to anyone with any insight here.

image.png

image.png

Kevin Buzzard (Jun 16 2021 at 16:26):

Can you post a #mwe rather than screenshots?

Eric Wieser (Jun 16 2021 at 17:13):

At a minimum you should move K [inhabited K] [field K] before the colon, unless the deriv you're not showing does something surprising

Andrew Elsey (Jun 16 2021 at 17:24):

Eric Wieser said:

At a minimum you should move K [inhabited K] [field K] before the colon, unless the deriv you're not showing does something surprising

I've been trying placing the K in several places (also as a variable, etc). That didn't seem to change the underlying problem, however. Oh well. Might just have to do a different approach. Thank you.

Eric Wieser (Jun 17 2021 at 11:21):

You'd likely get better help if you could provide a #mwe


Last updated: Dec 20 2023 at 11:08 UTC