------------------------------------------------------------------------ -- Modules that can (perhaps) not be type-checked in safe mode, and -- do not use --sized-types ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --irrelevant-projections #-} module README.Unsafe where -- Strings. import String -- IO. import IO-monad -- Squashing using irrelevance (with irrelevant projections). import Squash.Irrelevance