The Theory list
 Parents
 ℕ
 Children
 char
 Constants
 IsListRep (ℕ → 'a) × ℕ → BOOL [] 'a LIST Cons 'a → 'a LIST → 'a LIST Length 'a LIST → ℕ Hd 'a LIST → 'a Tl 'a LIST → 'a LIST Append 'a LIST → 'a LIST → 'a LIST Rev 'a LIST → 'a LIST Split ('a × 'b) LIST → 'a LIST × 'b LIST Combine 'a LIST → 'b LIST → ('a × 'b) LIST Map ('a → 'b) → 'a LIST → 'b LIST Fold ('a → 'b → 'b) → 'a LIST → 'b → 'b
 Aliases
 @ Append : 'a LIST → 'a LIST → 'a LIST
 Types
 '1 LIST
 Fixity
 Right Infix 300: @
 Definitions
 IsListRep is_list_rep_def ⊢ ∃ nil cons • IsListRep nil ∧ (∀ x• IsListRep x ⇒ (∀ h• ¬ cons h x = nil)) ∧ (∀ x y • IsListRep x ∧ IsListRep y ⇒ (∀ a b • cons a x = cons b y ⇔ a = b ∧ x = y)) ∧ (∀ x • IsListRep x ⇒ (∀ h• IsListRep (cons h x))) ∧ (∀ p • p nil ∧ (∀ m• p m ⇒ (∀ h• p (cons h m))) ⇒ (∀ n• IsListRep n ⇒ p n)) LIST list_def ⊢ ∃ f• TypeDefn IsListRep f Nil Cons nil_cons_def ⊢ (∀ x list• ¬ Cons x list = []) ∧ (∀ x1 x2 list1 list2 • Cons x1 list1 = Cons x2 list2 ⇔ x1 = x2 ∧ list1 = list2) ∧ (∀ p • p [] ∧ (∀ list• p list ⇒ (∀ x• p (Cons x list))) ⇒ (∀ list• p list)) Length length_def ⊢ # [] = 0 ∧ (∀ h list• # (Cons h list) = # list + 1) Hd hd_def ⊢ ∀ h list• Head (Cons h list) = h Tl tl_def ⊢ ∀ h list• Tail (Cons h list) = list Append append_def ⊢ (∀ list• [] @ list = list) ∧ (∀ h list list' • Cons h list @ list' = Cons h (list @ list')) Rev rev_def ⊢ Rev [] = [] ∧ (∀ h list• Rev (Cons h list) = Rev list @ [h]) Split split_def ⊢ Split [] = ([], []) ∧ (∀ list h1 h2 • Split (Cons (h1, h2) list) = (Cons h1 (Fst (Split list)), Cons h2 (Snd (Split list)))) Combine combine_def ⊢ Combine [] [] = [] ∧ (∀ h1 h2 list1 list2 • Combine (Cons h1 list1) (Cons h2 list2) = Cons (h1, h2) (Combine list1 list2)) Map map_def ⊢ (∀ g• Map g [] = []) ∧ (∀ h g list • Map g (Cons h list) = Cons (g h) (Map g list)) Fold fold_def ⊢ (∀ g x• Fold g [] x = x) ∧ (∀ h g x list • Fold g (Cons h list) x = g h (Fold g list x))
 Theorems
 list_induction_thm ⊢ ∀ p • p [] ∧ (∀ list• p list ⇒ (∀ x• p (Cons x list))) ⇒ (∀ list• p list) list_prim_rec_thm ⊢ ∀ n c • ∃1 f • f [] = n ∧ (∀ list a • f (Cons a list) = c a (f list) list) list_clauses ⊢ ∀ x1 x2 list1 list2 • ¬ Cons x1 list1 = [] ∧ ¬ [] = Cons x1 list1 ∧ (Cons x1 list1 = Cons x2 list2 ⇔ x1 = x2 ∧ list1 = list2) ∧ Head (Cons x1 list1) = x1 ∧ Tail (Cons x1 list1) = list1 list_cases_thm ⊢ ∀ list1 • list1 = [] ∨ (∃ x list2• list1 = Cons x list2)