The Coq mailing list

[Mandy Martino <tesleft AT hotmail.com>]

Hi  ,

when i continue to run,  got  some  error

[Loading ML file quote_plugin.cmxs ... done]

[Loading ML file newring_plugin.cmxs ... done]

[Loading ML file omega_plugin.cmxs ... done]

Coq < Coq < Coq < Coq < Error: tree already exists.

Coq < Inductive In (x:Z) : tree -> Prop :=

| In_left : forall l r y, (In x l) -> (In x (Node l y r))

| In_right : forall l r y, (In x r) -> (In x (Node l y r))

| Is_root : forall l r, (In x (Node l x r)).

Definition is_empty (s:tree) : bool := match s with

| Empty => true

| _ => false end.Coq < Coq < Coq < Toplevel input, characters 192-193:

> | Is_root : forall l r, (In x (Node l x r)).

>                                       ^

Error: In environment

In : Z -> tree -> Prop

x : Z

l : tree

r : ?8

The term "x" has type "Z" while it is expected to have type 

"tree".

Regards,

Martin 

> From: johnw AT newartisans.com
> To: tesleft AT hotmail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] how to run this program to verify a simple function?
> Date: Fri, 22 Jan 2016 17:48:17 -0800
>
> >>>>> Mandy Martino <tesleft AT hotmail.com> writes:
>
> > Error: The reference Z was not found in the current environment.
>
> I'm not sure whether the course defines Z some place, but otherwise you should
> just need:
>
> Require Import ZArith.
>
> --
> John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2