summaryrefslogtreecommitdiff
path: root/src/data/lib/prim/Agda/Builtin/Size.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/data/lib/prim/Agda/Builtin/Size.agda')
-rw-r--r--src/data/lib/prim/Agda/Builtin/Size.agda1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/data/lib/prim/Agda/Builtin/Size.agda b/src/data/lib/prim/Agda/Builtin/Size.agda
index 15daf1b..db4d510 100644
--- a/src/data/lib/prim/Agda/Builtin/Size.agda
+++ b/src/data/lib/prim/Agda/Builtin/Size.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --without-K #-}
module Agda.Builtin.Size where