Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Strict Implicit

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strict Implicit


chronological Thread 
  • From: Pierre Cast�ran <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
  • Date: Wed, 05 Dec 2007 20:44:36 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page