Standard Library

This section provides links to the theorems defined in the Deduce standard library along with the source files for the Deduce standard library.

• (Base.thm, Base.pf): Base proofs about propositional and predicate logic
• (Int.thm, Int.pf): Integers
• (List.thm, List.pf): Lists
• (Log.thm, Log.pf): Logarithms on natural numbers
• (Maps.thm, Maps.pf): Functional maps
• (MultiSet.thm, MultiSet.pf): Multisets
• (Nat.thm, Nat.pf): Natural numbers
• (Option.pf): Optional values
• (Pair.pf): Pairs
• (Set.thm, Set.pf): Sets
• (Sums.thm, Sums.pf): Proofs of summation formulae