The Coq mailing list

[Marianna Rapoport <mrapoport AT uwaterloo.ca>]

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)