1. First Steps🔗

The package is named complexitylib, and its modules begin with Complexity. and mirror CSLib's layout. import Complexity imports the whole library, which is convenient for exploring but slow to load; a development imports the modules it uses. Each module's documentation lists its main definitions and results, with references.

Declarations use CSLib's namespaces. Turing machines, encodings and polynomial-time computability live under Turing, and complexity classes, problems and reductions under Cslib.Complexity. For example, this chapter imports Complexity.Computability.Complexity.Classes.NP, which defines the class Cslib.Complexity.NP in terms of Turing.MultiTapeTM.ComputableInPolyTime:

@Cslib.Complexity.NP : {α : Type} → (α ↪ List Bool) → Set (Set α)

To find a declaration, search the API documentation. In this guide, hovering over a name shows its type and docstring, and clicking it opens its entry there.