From dfc231464492d09b02cd1c75f7802c45acca79d7 Mon Sep 17 00:00:00 2001 From: eldesh Date: Sat, 12 Oct 2024 18:28:31 +0900 Subject: [PATCH] fix typo --- examples/further-examples.gr.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/further-examples.gr.md b/examples/further-examples.gr.md index 48168a1f2..13bc00ea6 100644 --- a/examples/further-examples.gr.md +++ b/examples/further-examples.gr.md @@ -76,7 +76,7 @@ rest of the stack `xs` we use it once. An alternate definition of non-linearity on the elements: ~~~ granule -peek' : forall m : Ext Nat, a, n . Vec (n+1) (a [m..m+1]) -> (a, Vec (n+1) (a [m..m])) +peek' : forall {m : Ext Nat, a, n} . Vec (n+1) (a [m..m+1]) -> (a, Vec (n+1) (a [m..m])) peek' (Cons [x] xs) = (x, Cons [x] xs) ~~~