summaryrefslogtreecommitdiff
path: root/src/data/lib/prim/Agda/Builtin/IO.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/data/lib/prim/Agda/Builtin/IO.agda')
-rw-r--r--src/data/lib/prim/Agda/Builtin/IO.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/data/lib/prim/Agda/Builtin/IO.agda b/src/data/lib/prim/Agda/Builtin/IO.agda
index 4d15c24..cbc4388 100644
--- a/src/data/lib/prim/Agda/Builtin/IO.agda
+++ b/src/data/lib/prim/Agda/Builtin/IO.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --without-K #-}
module Agda.Builtin.IO where
@@ -6,4 +7,3 @@ postulate IO : ∀ {a} → Set a → Set a
{-# HASKELL type AgdaIO a b = IO b #-}
{-# COMPILED_TYPE IO MAlonzo.Code.Agda.Builtin.IO.AgdaIO #-}
-