Command-line options

We only list those options that can be given in .agda files in the {-# OPTIONS --opt₁ --opt₂ ... #-} form. Use agda --help for a complete list of options.

--with-K Overrides a global --without-K in a file (see Without K)
--without-K Disables definitions using Streicher’s K axiom (see Without K)