The Coq mailing list

[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


On Wed, Dec 05, 2007 at 07:34:59PM +0100, Stephane Le Roux wrote:
> 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

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46