The Coq mailing list

[Stephane Le Roux <stephane.le.roux AT ens-lyon.fr>]

Hello,

Thank you for the answers. Also, sorry for not being clear enough; I have to
rephrase my question: Coq says that the first argument of g is implicit,
despite the command Set Strict Implicit (I expected that g would have no
implicit argument). Is this the intended behaviour? If that's so, is there a
simple example that shows the difference between Set Strict Implicit and Unset
Strict Implicit?

Cheers,
Stephane




> Date: Wed, 05 Dec 2007 19:34:59 +0100
> From: Stephane Le Roux 
> <stephane.le.roux AT ens-lyon.fr>
> To: 
> coq-club AT pauillac.inria.fr
> Subject: [Coq-Club] Strict Implicit
>
> Hello,
>
> In the example below, Coq says that the first argument of a function 
> is implicit
> (despite the command Set Strict Implicit). Then, when trying to build a term
> with the function, Coq says that the first argument cannot be 
> inferred. Is this
> the intended behaviour? Did I do something wrong?
>
> Cheers,
> Stephane
>
> Coq < Set Implicit Arguments.
>
> Coq < Set Strict Implicit.
>
> Coq < Definition f (n : nat) := bool.
> f is defined
>
> Coq < Definition g(n: nat)(x:f n):= 0.
> g is defined
>
> Coq < Print g.
> g = fun (n : nat) (_ : f n) => 0
>     : forall n : nat, f n -> nat
>
>
> Argument n is implicit
> Argument scopes are [nat_scope _]
>
> Coq < Definition h:= g true.
> Toplevel input, characters 15-16
> > Definition h:= g true.
> >                ^
> Error: Cannot infer an instance for the implicit parameter n of g
>
>
> --__--__--
>
> Message: 2
> Date: Wed, 5 Dec 2007 20:33:44 +0100
> To: Stephane Le Roux 
> <stephane.le.roux AT ens-lyon.fr>
> Cc: 
> coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] Strict Implicit
> From: Jean-Francois Monin 
> <Jean-Francois.Monin AT imag.fr>
>
> Hi,
>
> Which value do you expect to be infered? Any expression e of type nat
> could be passed as an argument.
>
> Eg.:
> Definition h:= @g 3 true.
>
> Or:
> Variable x : nat.
> Definition h:= @g x true.
>
>
> Hope this helps,
>  JF Monin

> --__--__--
>
> Message: 3
> Date: Wed, 05 Dec 2007 20:44:36 +0100
> From: Pierre =?iso-8859-1?b?Q2FzdOlyYW4=?= 
> <pierre.casteran AT labri.fr>
> To: Jean-Francois Monin 
> <Jean-Francois.Monin AT imag.fr>
> Cc: Stephane Le Roux 
> <stephane.le.roux AT ens-lyon.fr>,
>        
> coq-club AT pauillac.inria.fr
> Subject: Re: [Coq-Club] Strict Implicit
>
>
> Hi,
>  You can also give an explicit type to true, and n is inferred:
>
>  Definition h := g (true: f 42).
>
> Pierre