The Coq mailing list

[Pierre Cast�ran <pierre.casteran AT labri.fr>]

Hi,
 You can also give an explicit type to true, and n is inferred:

 Definition h := g (true: f 42).

Pierre


Quoting 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club



Pierre Castéran