The Coq mailing list

[""Savi Maharaj"" <savi AT cs.stir.ac.uk>]

Dear Jean-Christophe,

Thanks for your reply. Unfortunately, I am still having trouble
getting Coq to accept my syntax. My impression is that there is some
problem with the use of implicit arguments within program expressions,
but maybe it is just that I haven't found the right syntax. I'll show
you a simple example of what I'm typing in and perhaps you can spot
what's wrong.

Here's the context:
  Require Correctness.
  Require PolyList.
  Global Variable l : (list nat) ref.

Then I try:

   Correctness silly_example l := (tail !l).

This gives me 
   Error: Illegal application (Type Error):
   The term tail of type (A:Set)(list A)->(list A)
   cannot be applied to the term
    l : (list nat)::Set
   This term has type (list nat)::Set which should be coercible to Set

I have tried adding the implicit argument (1!nat) but this seems to get
interpreted as an (unbound) reference. For example, if I type:

   Correctness silly_example l := (((tail) (1!nat)) !l).

I get the message:

   Error: Unbound reference nat

I have tried other combinations of parentheses but nothing works.

Savi