Options.lagda 367 B

1234567891011121314151617181920212223242526
  1. \documentclass{article}
  2. \usepackage{agda}
  3. \begin{document}
  4. \begin{code}
  5. {-# OPTIONS --no-positivity-check
  6. --no-termination-check
  7. -v 0 #-}
  8. {-# FOREIGN GHC
  9. f :: Maybe Bool -> Bool
  10. f Nothing = False
  11. f (Just True) = True
  12. f (Just False) = False
  13. #-}
  14. postulate
  15. A B : Set
  16. {-# DISPLAY A = B #-}
  17. \end{code}
  18. \end{document}