fix example/test

granule-project · Oct 17, 2024 · 094c905 · 094c905
1 parent 9896176
commit 094c905
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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]
 ~~~