agda/test/LaTeXAndHTML/succeed/Options.lagda

\documentclass{article}

\usepackage{agda}

\begin{document}

\begin{code}
{-# OPTIONS --no-positivity-check
            --no-termination-check
            -v 0 #-}

{-# FOREIGN GHC
  f :: Maybe Bool -> Bool
  f Nothing        = False
  f (Just  True)   = True
  f (Just  False)  = False
  #-}

postulate
  A B : Set

{-# DISPLAY A = B #-}
\end{code}

\end{document}