Enzo Crance (Oct 25 2022 at 09:16): Enzo Crance (Oct 25 2022 at 09:16):Hello. I got Anomaly "match on unknown, non singleton, inductive" when trying to elaborate a freshly generated term. The error is likely triggered there. It's when Elpi gives the term to Coq before elaboration. The error comes from a match in Elpi, and the only one I have in my term is the following:
match c7
(prod (X0^3 c3 c4 c5)
(app [pglobal (indt «list») «Test.783», c3]) c8 \
app [pglobal (indt «list») «Test.783», c4])
[ ... ]
idk what is ill-formed in this. c3 c4 are bound types higher in the term, c7 is a term in list c3. I'm just matching a list A and building a list B essentially
Enrico Tassi (Oct 25 2022 at 09:32):The syntax for match is tricky because Elpi must be able to know the name of the inductive type being inspected. It reads it from the return clause, which is a function taking the eliminated term (and its indexes if any) and returning a type. In you case it should be
fun l : list A => list B
but it seems you wrote
list A -> list B
Enrico Tassi (Oct 25 2022 at 09:33): Enrico Tassi (Oct 25 2022 at 09:34):I guess the error message should be more precise, like "I found list A -> list B, but I was expecting a lambda"
Enzo Crance (Oct 25 2022 at 09:34):Ok thanks, I mixed prod and fun
Last updated: Oct 13 2024 at 01:02 UTC