coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cedric Auger <sedrikov AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Inconsistent handling of implicit record type parameters
- Date: Fri, 5 Dec 2014 16:18:07 +0100
2014-12-05 15:53 GMT+01:00 <michael.soegtrop AT intel.com>:
For me, in your example Print and Print Implicit seem to be consistent.
Both tell that mkRecTest has no implicit arguments (although RecTest itself has implicit arguments).
Until you decide to put the first argument of mkRecTest (par) implicit, and then both report it as implicit.
To sum up, when you write:
Record RecTest {par : nat} : Type := mkRecTest
{
elem1 : nat
}.
You tell coq to consider "par" as implicit for RecTest, but you do not tell what to do with the "par" argument of mkRecTest. Coq uses an heuristic which tells that it is probably a bad idea to set this argument as implicit, as it cannot easily infer it. For instance, "mkRecTest 8 : RecTest" does not provide much information on the "par" parameter.
Dear Coq users,
I have a problem with implicit record type arguments defined via {} binders.
Print and Print Implicit show different status on wether such parameters are
implicit or not, and it doesn't work as expected. Please have a look at the
Coq code below. Is therer an explanation for this behaviour, or is this a bug?
For me, in your example Print and Print Implicit seem to be consistent.
Both tell that mkRecTest has no implicit arguments (although RecTest itself has implicit arguments).
Until you decide to put the first argument of mkRecTest (par) implicit, and then both report it as implicit.
To sum up, when you write:
Record RecTest {par : nat} : Type := mkRecTest
{
elem1 : nat
}.
You tell coq to consider "par" as implicit for RecTest, but you do not tell what to do with the "par" argument of mkRecTest. Coq uses an heuristic which tells that it is probably a bad idea to set this argument as implicit, as it cannot easily infer it. For instance, "mkRecTest 8 : RecTest" does not provide much information on the "par" parameter.
Best regards,
Michael
Record RecTest {par : nat} : Type := mkRecTest
{
elem1 : nat
}.
Print mkRecTest.
(*
Record RecTest (par : nat) : Type := mkRecTest { elem1 : nat }
For RecTest: Argument par is implicit and maximally inserted
For RecTest: Argument scope is [nat_scope]
For mkRecTest: Argument scopes are [nat_scope nat_scope]
=> This is what I expected
*)
Print Implicit mkRecTest.
(*
mkRecTest : forall par : nat, nat -> RecTest
=> Here par is not mentioned as implicit
=> Also I have to give the argument explicitly
*)
Definition test : @RecTest 1 := mkRecTest _ 1.
(* Define par more explicitly as implicit *)
Arguments mkRecTest [par] _.
Print mkRecTest.
(*
Record RecTest (par : nat) : Type := mkRecTest { elem1 : nat }
For RecTest: Argument par is implicit and maximally inserted
For mkRecTest: Argument par is implicit
For RecTest: Argument scope is [nat_scope]
For mkRecTest: Argument scopes are [nat_scope nat_scope]
*)
Print Implicit mkRecTest.
(*
mkRecTest : forall par : nat, nat -> RecTest
Argument par is implicit
*)
Definition test2 : @RecTest 1 := mkRecTest 1.
(* => Now everything works fine *)
--
.../Sedrikov\...
- [Coq-Club] Inconsistent handling of implicit record type parameters, michael.soegtrop, 12/05/2014
- Re: [Coq-Club] Inconsistent handling of implicit record type parameters, Cedric Auger, 12/05/2014
- RE: [Coq-Club] Inconsistent handling of implicit record type parameters, Soegtrop, Michael, 12/08/2014
- Re: [Coq-Club] Inconsistent handling of implicit record type parameters, Cedric Auger, 12/05/2014
Archive powered by MHonArc 2.6.18.