Stream: Coq users

Topic: Conflict between Ltac syntax and custom notation

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

Simon Hudon (Jun 15 2020 at 20:21):

Is there a way to disambiguate?

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.

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?

Kenji Maillard (Jun 16 2020 at 13:34):

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

Simon Hudon (Jun 16 2020 at 14:31):

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

Last updated: Sep 23 2023 at 06:01 UTC