The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

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?

Inductive type : Type :=
| TBool : type.

Inductive term1 : Type :=
| tvar1 : term1.

Inductive term2 : Type :=
| tvar2 : term2.

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

Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.
Notation "G '⊢' t '::' T" := (vdash G t T) (at level 40, t at level 59).

Inductive typing1 : VDash context term1 type :=
| T_Var1 : forall G T,
    G ⊢ tvar1 :: T

with typing2 : VDash context term2 type :=
     | T_Var2 : forall G T,
         G ⊢ tvar2 :: T.