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: Oct 13 2024 at 01:02 UTC