This section provides links to the theorems defined in the Deduce standard library along with the source files for the Deduce standard library.
Only the top-level module files (such as UInt.pf) are listed below. Each module may be split internally across several private helper files (for example, UIntAdd.pf, UIntMult.pf, ...) that are publicly imported from the main module file; users should import the module by its top-level name.
Base.thm, Base.pf): Base proofs about propositional and predicate logicBigO.thm, BigO.pf): Big-O asymptotic analysis on fn UInt -> UIntInt.thm, Int.pf): IntegersList.thm, List.pf): ListsMaps.thm, Maps.pf): Functional mapsMultiSet.thm, MultiSet.pf): MultisetsNat.thm, Nat.pf): Natural numbersOption.pf): Optional valuesPair.pf): PairsSet.thm, Set.pf): SetsUInt.thm, UInt.pf): Unsigned integers