(** check equality between natural numbers **)

(** Propositional equality **)
Check 3=4.

(** Boolean equality **)
Require Import Arith.
Check beq_nat 3 4.
Eval compute in beq_nat 3 4.

(** evaluating "(3=4) and true" **)
Eval compute in andb (beq_nat 3 4) true.




(** is_zero for natural numbers **)

Definition is_zero (n:nat) :=
  match n with
    0 => true
  | S p => false
  end.

Eval compute in is_zero 0.

(** negative numbers are treated as "0" **)
Eval compute in is_zero (5-6).




(** is_zero for integers **)
Require Import ZArith.


(** Z.add is the function which adds two integers **)

(** prints the type **)
Check Z.add.
(** prints the definition **)
Print Z.add.
Eval compute in Z.add 5 (Zneg 6).

(** is_zero is only defined for natural numbers; so, the following
returns with a type error

Eval compute in is_zero(Z.add 5 (Zneg 6)).

**)

(** Z is the integer type. It has three constructors - for zero, positive
and negative integers **)
Print Z.

(** new definition for is_zero for integers **)
Definition z_is_zero (z : Z) :=
  match z with
    Z0 => true
  | Zpos p => false
  | Zneg n => false
  end.

Eval compute in z_is_zero (5-6).