aboutsummaryrefslogtreecommitdiff
path: root/Util.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Util.agda')
-rw-r--r--Util.agda1
1 files changed, 1 insertions, 0 deletions
diff --git a/Util.agda b/Util.agda
index b30aeb5..0c79b17 100644
--- a/Util.agda
+++ b/Util.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --without-K --safe #-}
module Util where
open import Data.Fin using (Fin; toℕ)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-18 10:49:01 +0000