coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Cannot infer implicit parameter when using notation in inductive definition
Date: Sat, 30 Sep 2017 02:22:47 +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-wm0-f52.google.com
Ironport-phdr: 9a23:Bm0FOR231cXJBbh3smDT+DRfVm0co7zxezQtwd8ZseseLfad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tLw6annrnpzUVA1D0MRd/DuXzAI/bycqtnajm8JrKJg5MmTCVYLVoLRzwox+H5ecMho43A6A9xwHS6l9VfehN2W5kORrHlhDw692r1Jdl/ylKoPY88cJbTaj2Y+IjQOoLX3wdL2kp6Ziz5lH4RgyV6y5EXw==

Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop :=
| c1 m : P m
| c2 m : *m
where "* m" := (P m).

Why do I get an error "Cannot infer the implicit parameter n of P ..."
for constructor c2 but not for constructor c1?

[Coq-Club] Cannot infer implicit parameter when using notation in inductive definition, Anders Lundstedt, 09/30/2017
- Re: [Coq-Club] Cannot infer implicit parameter when using notation in inductive definition, Hugo Herbelin, 09/30/2017