Hi. I was trying to a search function for a binary search tree as in part 3 of the software fundametals book here.

```
From Coq Require Import String.
Require Import Coq.Arith.PeanoNat.
Require Import Notations.
Notation "a >? b" := (Nat.ltb b a)
(at level 70) : nat_scope.
Definition key := nat.
Inductive tree (V : Type) : Type :=
| E
| T (l : tree V) (k : key) (v : V) (r : tree V).
Arguments E {V}.
Arguments T {V}.
Fixpoint isBound {V : Type} (x : nat) (t : tree V) : bool :=
match t with
| E => false
| T left key val right => if x <? key then (isBound x left)
else if x >? key then (isBound x right)
else true
end.
```

But I get an error on `isBound`

saying

```
The constructor left (in type sumbool) expects 1 argument.
```

Why is that error showing up? Couldn't figure it out.

The error says that `left`

is a constructor of an inductive defined in your context, namely `sumbool`

:

```
Print sumbool.
(* Inductive sumbool (A B : Prop) : Set := *)
(* left : A -> {A} + {B} | right : B -> {A} + {B} *)
(* *)
(* Arguments sumbool (_ _)%type_scope *)
(* Arguments left {A B}%type_scope, [A] _ _ *)
(* Arguments right {A B}%type_scope, _ [B] _ *)
```

so you cannot use `left`

or `right`

as identifiers in a pattern of a pattern-match construct (change `left`

and `right`

to `l`

/`r`

and everything is fine)

Oh.. so it's because there's already a name `left`

. Thanks!

Ju-sh has marked this topic as resolved.

Last updated: Jun 25 2024 at 14:01 UTC