Clever Geek Handbook

Why can't I identify the next CoFixpoint?

I use:

$ coqtop -v
The Coq Proof Assistant, version 8.4pl5 (February 2015)
compiled on Feb 06 2015 17:44:41 with OCaml 4.02.1

I have identified the following type CoInductive

, stream

:

$ coqtop
Welcome to Coq 8.4pl5 (February 2015)

Coq < CoInductive stream (A : Type) : Type := 
Coq < | Cons : A -> stream A -> stream A.
stream is defined

Coq < Check stream.
stream
     : Type -> Type

Coq < Check Cons.
Cons
     : forall A : Type, A -> stream A -> stream A

Then I tried to determine the following definition CoFixpoint

, zeros

:

Coq < CoFixpoint zeros : stream nat := Cons 0 zeros.

However, I got the following error instead:

Toplevel input, characters 38-39:
> CoFixpoint zeros : stream nat := Cons 0 zeros.
>                                       ^
Error: In environment
zeros : stream nat
The term "0" has type "nat" while it is expected to have type 
"Type".

I realized that I need to explicitly specify the variable A

:

Coq < CoFixpoint zeros : stream nat := Cons nat 0 zeros.
zeros is corecursively defined

Why isn't Coq emitting a type A

by itself? How do I infer the type A

?

+3


source to share


1 answer


You need to declare A

as implicit in order to ask Coq to do this for you. There are several ways to do this:

  • Add to your following declaration: Set Implicit Arguments.

    . This will force Coq to enable auto-inference for arguments such as A

    for Cons

    , allowing you to write Cons 0 zeros

    .

  • Include implicit arguments for only Cons

    , without affecting the rest of the file:

    Arguments Cons {A} _ _.

    This declaration is marked A

    as implicit and leaves the other two arguments explicit.

  • Mark A

    as implicit in the definition stream

    :

    CoInductive stream {A : Type} : Type := 
| Cons : A -> stream A -> stream A.

    I personally don't recommend doing this as it will mark A

    as implicit for stream

    .



More information on implicit arguments can be found in the reference manual

+4


source






More articles:


All Articles