From 74d0b7259822a40845d1c006a6e021449eb58564 Mon Sep 17 00:00:00 2001
From: Dominic Orchard <dom.orchard@gmail.com>
Date: Thu, 17 Oct 2024 13:46:26 +0100
Subject: [PATCH] fix example/test

---
 examples/intro.gr.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/intro.gr.md b/examples/intro.gr.md
index aea33ca06..51264cc87 100644
--- a/examples/intro.gr.md
+++ b/examples/intro.gr.md
@@ -555,7 +555,7 @@ leak = hash secret
 (`gr examples/intro.gr.md --literate-env-name grill7`)
 
 ~~~ granule
-hash : forall {l : Level} . Int [l] -> Int [l]
+hash : forall {l : Sec} . Int [l] -> Int [l]
 hash [x] = [x*x*x]
 ~~~