(** Scoping **)

Check 3.
Require Import ZArith.
Check 3.

Open Scope Z_scope.
Check 3.
Print Scope Z_scope.

Eval compute in 5-7.
Eval compute in (-5)*(-5).
Check 3.

Require Import Arith.
Check 3.
Close Scope Z_scope.

Check 3%Z.
Check (-3)%Z.

Require Import ZArith.
Open Scope Z_scope.
Check -3.

Require Import Arith.
Open Scope nat_scope.
Check 3.
Check (-3)%Z.
Check plus 3.
Check Z.mul (-5).

Check 3.





(** Rationals **)

Require Import ZArith.
Open Scope Z_scope.
Require Import QArith.
Open Scope Q_scope.
Check 3.
Print Scope Q_scope.
Eval compute in 5#4.
Eval compute in (5#4)-(1#4).
Eval compute in (4#4)>(3#7).
Eval compute in (1#1)/(3#4).
Check (3#1)%Q.
Close Scope Q_scope.
Eval compute in 5 - 7. (** WHAT'S THE PROBLEM HERE? **)
Open Scope Z_scope.
Eval compute in 5-7.
Close Scope Z_scope.





Require Import ZArith.

Fixpoint evenb n :=
  match n with
    0 => true
  | 1 => false
  | S (S p) => evenb p
  end.

Check evenb.

Eval compute in evenb 10001.
Eval compute in evenb 10002.






(** Lists **)

Require Import List.
Eval compute in 1::2::3::nil.
Eval compute in  (1%Z)::(2%Z)::(3%Z)::nil.
Check nil.
Check nil:list nat.
(** this gives error :
Check 1::(-2)%Z::nil. **)