Be explicit about where erasure is actually needed.

lemastero · Dec 15, 2023 · 1830fbc · 1830fbc
1 parent 2b7edd7
commit 1830fbc
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/examples/nat.agda b/examples/nat.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --erasure #-}
+
 data Nat : Set where
   Zero : Nat
   Succ : Nat → Nat
@@ -6,7 +8,7 @@ add : Nat → Nat → Nat
 add n Zero = n
 add n (Succ m) = Succ (add n m)
 
-data Eq {A : Set} (a : A) : A → Set where
+data Eq {A : Set} (@0 a : A) : @0 A → Set where
   Refl : Eq a a
 
 cong : {A B : Set} → {a b : A} → (f : A → B) → Eq a b → Eq (f a) (f b)