diff --git a/examples/further-examples.gr.md b/examples/further-examples.gr.md index 48168a1f..13bc00ea 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) ~~~