Stream: Equations devs & users

Topic: Weird syntax error with `by struct`


view this post on Zulip 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?

view this post on Zulip Théo Winterhalter (Jun 07 2021 at 06:20):

Do you still have it if you add a space before :=? (Just a random thought.)

view this post on Zulip 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:=

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Jun 09 2021 at 09:43):

I think it's the dreaded ident/keyword mixup. I'll try something

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Jun 09 2021 at 10:08):

Hmm, I can't reproduce the problem actually

view this post on Zulip Matthieu Sozeau (Jun 09 2021 at 10:10):

Ah I think I got it, using IDENT "struct" works better


Last updated: Jan 29 2023 at 15:02 UTC