coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marianna Rapoport <mrapoport AT uwaterloo.ca>
- To: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Overloading notation for different types in Coq
- Date: Thu, 18 May 2017 15:27:03 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mrapoport AT uwaterloo.ca; spf=Pass smtp.mailfrom=mrapoport AT uwaterloo.ca; spf=None smtp.helo=postmaster AT minos.uwaterloo.ca
- Dkim-filter: OpenDKIM Filter v2.11.0 minos.uwaterloo.ca v4IJR4wC022185
- Ironport-phdr: 9a23:1KFbVhwF20ACA5jXCy+O+j09IxM/srCxBDY+r6Qd2+0eIJqq85mqBkHD//Il1AaPBtSFra8bw6qO6ua7CDNGuc7A+Fk5M7VyFDY9yv8q1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twvcu80XjId4Kqs8yAbCrn9Ud+hL329lK1aekhTm6sus4JJv9jlbtu48+cJHTaj1cKM0QKBCAjghL247+tDguwPZTQuI6HscU2EWnQRNDgPY8hz0XYr/vzXjuOZl1yaUIcP5TbYvWTS/9KhrUwPniD0GNzEi7m7ajNF7gb9BrxKgoxx/xJPUYJ2QOfFjcK7RYc8WSGxcVctKSSdPHp2zYJcOD+oZPOZXsY/9p0cVrRCjAQWgHf7jxiNUinPz26AxzuYvHhzc3AE4HNwAsGrao9r6OqgOVu67wqfIwjfeYf5NxTf98ZLFfgw7rP2QX799d9fax0k1FwPCi1WdsYvrMCmP1uQMqWeb6exgWviygGA7sQ5xuj+vxt8rionTmoIe11fJ9SBjwIkvPd24T1Z7Ydm+EJtMrCyaKoV3Tdk+Q252oiY6zroGuZmhcCcW0psq3hjSYOGEfYiQ+h/vSfidLDNiiH9her+znQu+/Vajx+HmVMS5005GoytEn9XWq3wBygHf5tKIR/dn4EutxzSC2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmEX3iq+WcV4k9vK16+XpeLrmuoGTN5VwigH5NaQigNCwDv4gPggPWWiU5/i82aX+8UHnRLhGlPk7n6vDvJzHO8gWpbS1Dg1W34o77hawFTam0NAWnXkdK1JFfQqKj43zO17UOPD4Cu+/g1O2kDd33P3GI7PgDY/RLnfdirfhebF960lGxAUv199T/4hUBa0ZIPLvRk/xs8TVAQM+Mwyt2uroFNF91p4FVm+UGa+YMKbSsUeS6e41IumMYpUVuDfnJPQ/6f7ulyxxpVhIUqCkwZIRIF+5Gv5rOVnRNXXlj8sIFyEFvw40Qfb2oFCESntXdnG0GawmsHVzA4W/SIzHW4qFgbqb3S79EIcFSHpBDwWpGG3pfoOCUr82YTqVOsh7jnRQUKKoU4g50guynBLlwqZqNO7T/WsTvMSwh5BO++TPmERqpnRPBMOH3jTIFjkskw==
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)
- [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/18/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/18/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Gaetan Gilbert, 05/18/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/18/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/19/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Abhishek Anand, 05/20/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/21/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Abhishek Anand, 05/20/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/19/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/18/2017
Archive powered by MHonArc 2.6.18.