summaryrefslogtreecommitdiff
path: root/src/data/lib/prim/Agda/Primitive.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/data/lib/prim/Agda/Primitive.agda')
-rw-r--r--src/data/lib/prim/Agda/Primitive.agda2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/data/lib/prim/Agda/Primitive.agda b/src/data/lib/prim/Agda/Primitive.agda
index b2b7b37..a73dd30 100644
--- a/src/data/lib/prim/Agda/Primitive.agda
+++ b/src/data/lib/prim/Agda/Primitive.agda
@@ -1,5 +1,7 @@
-- The Agda primitives (preloaded).
+{-# OPTIONS --without-K #-}
+
module Agda.Primitive where
------------------------------------------------------------------------