Topic: using recursor to write term
Kevin Buzzard (Nov 13 2019 at 13:26):
I'm trying to be a computer scientist, unsuccessfully. I'm trying to define a function in term mode.
inductive C : Type | c1 : C | c2 : C inductive D : Type | d1 : D | d2 : D def thing1 (c : C) (d : D) : D := c.rec (_) -- correct "don't know how to synthesize placeholder -- here's a helpful context" (_) -- correct def thing2 (c : C) (d : D) : D := c.rec (d.rec _ _) (_) /- type mismatch at application C.rec (D.rec ?m_3 ?m_4 d) term D.rec ?m_2 ?m_3 d has type ?m_1 d : Sort ? but is expected to have type ?m_1 C.c1 : Sort ? -/
thing1 is where things are going well. I want to use recursion on
c and so I write
c.rec _ _ and both underscores have nice red underlines, indicating that I'm on the right track.
But then I want to use recursion on
d too, so I edit
thing1 until it becomes
thing2 and instead of having now three nice red underlines under my three underscores, Lean just gives up, flags the
c.rec as an error. In reality the two inductive types are far more complicated and have parameters etc.
Is there some trick to persuade Lean to start telling me the local context at every underscore? Have I just made some more basic error? It is going to be a royal pain figuring out all the types in my use case (some proofs are involved, I will need to drop into tactic mode at some point to supply all the terms needed).
Am I missing a trick? Have I made an error?
Chris Hughes (Nov 13 2019 at 13:27):
D.rec_on d. I think there's a bug where it doesn't use the
elab_as_eliminator when you use projection notation
Chris Hughes (Nov 13 2019 at 13:29):
Kevin Buzzard (Nov 13 2019 at 13:49):
I think I love you. Many thanks!
Kevin Buzzard (Nov 13 2019 at 14:13):
Works in my real use case too :D I'm sure this has caused me problems on several occasions in the past. It's only now I am confident enough to start saying "I think this should work" rather than just saying "maybe I need to understand things better".
Kevin Buzzard (Nov 13 2019 at 14:14):
@Ellen Arlt I can write that function now.
Last updated: May 17 2021 at 21:12 UTC