Stream: Coq users

Topic: Conflict between Ltac syntax and custom notation


view this post on Zulip Simon Hudon (Jun 15 2020 at 20:21):

Hi! I'm going through Software Foundations an in the section on types, the notation Gamma |- t \in T is defined. I run into problem in this chapter when trying to write tactics with a match goal:

match goal with
  | [ H : ?v |- _ ] => idtac T
(* Error:
Syntax error: '\in' expected after [constr:operconstr level 200] (in [constr:operconstr]).
*)
  end

view this post on Zulip Simon Hudon (Jun 15 2020 at 20:21):

Is there a way to disambiguate?

view this post on Zulip Paolo Giarrusso (Jun 16 2020 at 11:28):

Probably not without changing SF, but can you link to the problematic SF definition? I checked some SF chapters, and they seem to use ⊢ instead of the ascii version (e.g. https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html#lab216), which is probably the easiest fix.

view this post on Zulip Simon Hudon (Jun 16 2020 at 13:26):

Nice, thanks! I must be using an older version. This is exactly the chapter I'm looking at. What is the trick in emacs to input those unicode characters?

view this post on Zulip Kenji Maillard (Jun 16 2020 at 13:34):

If you are using company-coq, you can obtain it with \vdash

view this post on Zulip Simon Hudon (Jun 16 2020 at 14:31):

Thanks! I think I might have set it wrong. I'll have another go


Last updated: Feb 04 2023 at 20:02 UTC