add pragma and comment in Hello example

lemastero · Nov 21, 2023 · 474889b · 474889b
1 parent 45dd2e1
commit 474889b
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/test/Hello.agda b/test/Hello.agda
@@ -1,9 +1,12 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module test.Hello where
 
+-- Type with two inhabitants
 data Bool : Set where
-  true : Bool
-  false : Bool
+  false true : Bool
 
+{- Logical connective not - negation -}
 not : Bool -> Bool
 not true  = false
 not false = true