coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Cannot infer implicit parameter when using notation in inductive definition

From: Anders Lundstedt <anders AT anderslundstedt.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Cannot infer implicit parameter when using notation in inductive definition
Date: Mon, 2 Oct 2017 00:33:51 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=anders AT anderslundstedt.se; spf=Pass smtp.mailfrom=anders AT anderslundstedt.se; spf=None smtp.helo=postmaster AT mail-wr0-f174.google.com
Ironport-phdr: 9a23:vYCeMRXi6YPMGaa2KMaGcraX0F7V8LGtZVwlr6E/grcLSJyIuqrYZRyAt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl8/LePsX4XWks6f1uao+pSVbR8CzG62Zqo3JxGrpy3QsNMXiM1sMPBi5AHOpy5hfehb33ggAU+Vkw3g68ustMpq9ShdoekJ/shMXL/he7k+QadEATg6dXs4sp64/SLfRBeCsyNPGl4dlQBFVlDI

> This is a (known) limitation of the combination of "Inductive",
> "where" and implicit parameters.

I see, thanks for the clarification.

> You could fill a bug report so that something is eventually done to
> improve this.

Done:

https://coq.inria.fr/bugs/show_bug.cgi?id=5762

Re: [Coq-Club] Cannot infer implicit parameter when using notation in inductive definition, Anders Lundstedt, 10/02/2017