Require Import Bool Arith List. (* DEMO 1 *) Check true. Check false. Check true && false. Compute true && false. Compute true && negb false. Check 7. Check 3 + 7. Compute 3 + 7. (* DEMO 2 *) Definition myfunc (x : nat) := x + x. Check myfunc. Check myfunc 4. Compute myfunc 5. Fail Check myfunc true. Compute let tmp := myfunc 7 in tmp + tmp. Check fun x : nat => x + x. Compute let f := fun x : nat => x + x in f (f 3). Definition myfunc2 (x : nat) (y : nat) := x + y. Check myfunc2. Check myfunc2 7. Check myfunc2 7 3. Compute myfunc2 7 3. (* DEMO 3 *) Locate "_ * _". Compute mult 2 3. Check (3, 4). Locate "_ * _". Check list. Check list nat. (* DEMO 4 *) Definition add_pair (p : nat * nat) := match p with | (n,m) => n + m end. Compute add_pair (3,2). Print nat. Definition is_4 (n : nat) := match n with | 4 => true | _ => false end. Compute is_4 7. Compute is_4 4. Check (if true then 0 else 1). (* DEMO 5 *) Fixpoint mlnat (l : list nat) := match l with | nil => 0 | x :: xs => x * mlnat xs end. Fail Fixpoint wrong (l : list nat) := match l with | nil => wrong (17 :: nil) | x :: xs => x + wrong xs end. Fixpoint list_forall (p : nat -> bool) (l : list nat) := match l with | nil => true | x :: xs => (p x) && (list_forall p xs) end. Compute list_forall (fun x => leb x 17) (33 :: 4 :: nil).