coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Strict Implicit, Stephane Le Roux
- Re: [Coq-Club] Strict Implicit,
Jean-Francois Monin
- Re: [Coq-Club] Strict Implicit, Pierre Castéran
- Re: [Coq-Club] Strict Implicit, Hugo Herbelin
- Re: [Coq-Club] Strict Implicit,
Jean-Francois Monin
Archive powered by MhonArc 2.6.16.