Check True.
Check true.
Check 3.
(* no decimal numbers *)
Check (3+4).
(* how to deal with negative number? *)
Check (3=4).
Check (3,4).
Check (3,4,5).
Check ((3=5) /\ True).

Check and.
Check (fun x: nat => x=3).

Check (let f := fun x => (x*3, x) in f 3).

Locate "_ <= _".

Definition example1 := fun x:nat => x*x + x + 1.
Eval compute in
  let f := fun x => (x+3, x) in f 3.

Eval compute in
  let g := fun x y => (orb x y) in g true false.

(** Require Import Arith.

Check beq_nat 3 4.
**)

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

Eval compute in is_zero 0.

Eval compute in is_zero (5-6).

(** Require Import ZArith.
Open Scope Z_scope.

Print Z.

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). **)

Fixpoint sum_n2 n s :=
  match n with
    0 => s
  | S p => p + sum_n2 p (p + s)
  end.

Eval compute in sum_n2 10 5.