Require Import Arith Bool List. Definition add2 x := x + 2. Check add2 3. \textcolor{blue}{add2 3 : nat} Compute add2 3. Definition twice (f : nat -> nat) (x : nat) := f (f x). Compute twice (twice add2) 1. Definition headplus1 (l : list nat) := match l with a :: l1 => a + 1 | nil => 0 end. Fixpoint grow_nat (l : list nat) := match l with nil => nil | a :: l1 => 2 * a :: 2 * a + 1 :: grow_nat l1 end. Fixpoint my_filter {T : Type} (p : T -> bool) (l : list T) : list T := match l with nil => nil | a :: l1 => if p a then a :: my_filter p l1 else my_filter p l1 end.