## 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: Feb 04 2023 at 20:02 UTC