------------------------------------------------------------------------ -- Safe modules that use --with-K ------------------------------------------------------------------------ {-# OPTIONS --safe --with-K #-} module README.Safe.With-K where -- Some theory of Erased, developed using the K rule and propositional -- equality. import Erased.With-K