The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Increasing the level of your notation (thereby reducing its "priority") helps:

Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.

Notation "G '|-' e '::' T" := (vdash G e T) (at level 999, e at level 59).

Ltac tactic :=

  solve [match goal with

  | H: _ |- _ => auto

  end].

  

Global Instance vd : VDash nat nat nat := fun a b c => True.

Check (0 |- 0::0).

(* The manual says that levels are supposed to be 200 or less, so I have no idea why 999 is allowed. 200 isn't high enough for the last Check to check*)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, May 19, 2017 at 4:59 PM, Marianna Rapoport <mrapoport AT uwaterloo.ca> wrote:

As a follow up on the turnstile notation, is it possible to avoid a parse conflict with the match notation of Ltac?

Minimal example:

Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.

Notation "G '|-' e '::' T" := (vdash G e T) (at level 40, e at level 59).

Ltac tactic :=

  solve [match goal with

  | H: _ |- _ => auto

  end].

The error I get is:

Syntax error: '::' expected after [constr:operconstr level 59] (in [constr:operconstr]).

On Thu, May 18, 2017, at 03:27 PM, Marianna Rapoport wrote:

> That's exactly what I was looking for. Thanks a lot!

>

> Marianna

>

> On Thu, May 18, 2017, at 02:05 PM, Gaetan Gilbert wrote:

> > With typeclasses you can do something like see attached file.

> >

> > Gaëtan Gilbert

> >

> > On 18/05/2017 19:57, Marianna Rapoport wrote:

> > > I would like to be able to define the same Coq notations for different

> > > inductive definitions, and distinguish the notations based on the

> > > types of their arguments.

> > >

> > > Here is a minimal example:

> > >

> > >     Inductive type : Type :=

> > >     | TBool : type.

> > >

> > >     Inductive term1 : Type :=

> > >     | tvar1 : term1.

> > >

> > >     Inductive term2 : Type :=

> > >     | tvar2 : term2.

> > >

> > >     Definition context := nat -> (option type).

> > >

> > >     Reserved Notation "G '⊢' t '::' T" (at level 40, t at level 59).

> > >

> > >     Inductive typing1 : context -> term1 -> type -> Prop :=

> > >      | T_Var1 : forall G T,

> > >           G ⊢ tvar1 :: T

> > >     where "G '⊢' t1 '::' T" := (typing1 G t1 T)

> > >     with typing2 : context -> term2 -> type -> Prop :=

> > >      | T_Var2 : forall G x T,

> > >           G ⊢ tvar2 :: T

> > >     where "G '⊢' t2 '::' T" := (typing2 G t2 T).

> > >

> > > As you see, there is a mutually inductive definition, in which I'd

> > > like to be able to use the same notation for different types of terms

> > > (`term1` and `term2`).

> > >

> > > The error I get when trying to compile this is `Error: Illegal

> > > application (Non-functional construction): The _expression_ "tvar1" of

> > > type "term1" cannot be applied to the term "x" : "?T"`.

> > >

> > > Is there a way to get this to work, maybe by using type classes?

> >

> > Email had 1 attachment:

> > + tc_notas.v

> >   1k (text/x-verilog)