Simon Hudon (Jun 07 2021 at 00:12): Simon Hudon (Jun 07 2021 at 00:12):Hi! I have the following signature for a definition using equations:
Equations value_repr (p : val) (v : lean_value unit) : iProp by struct v:= {
For some reason, Coq / Equations are reporting the following error:
Error: Syntax error: 'wf' or 'struct' expected after 'by' (in [wf_annot]).
Does this make sense to someone?
Théo Winterhalter (Jun 07 2021 at 06:20):Do you still have it if you add a space before :=? (Just a random thought.)
Simon Hudon (Jun 08 2021 at 03:06):The situation disappeared I believe after I saved my buffer. The current version still features this : iProp by struct v:=
Matthieu Sozeau (Jun 08 2021 at 07:42):There's a subtle bug with the handling of by I think, sometimes requiring a restart of the buffer. Side-effects in the grammar definition I believe.
Simon Hudon (Jun 08 2021 at 20:40):That's interesting. I didn't think that could be a useful solution. Is it somehow getting cached?
Matthieu Sozeau (Jun 09 2021 at 09:43):I think it's the dreaded ident/keyword mixup. I'll try something
Matthieu Sozeau (Jun 09 2021 at 10:07):@Pierre-Marie Pédrot does it make sense that if I put IDENT "by" in an mlg, we don't get this strange behavior?
Matthieu Sozeau (Jun 09 2021 at 10:08):Hmm, I can't reproduce the problem actually
Matthieu Sozeau (Jun 09 2021 at 10:10):Ah I think I got it, using IDENT "struct" works better
Last updated: May 28 2023 at 18:29 UTC