\begin{code}
{-# OPTIONS --without-K #-}
module Example where
\end{code}

%<*example>
\begin{code}
data ⊥ : Set where

record ⊤ : Set where constructor tt
\end{code}
%</example>