From 7c3eb38ce3bbf081da1f086d1af8f48d263dbd19 Mon Sep 17 00:00:00 2001 From: Anthony Carrico Date: Wed, 17 Apr 2019 11:18:44 -0400 Subject: [PATCH] Update tutorial's "using" example to avoid errors As a beginner, I just interpolated between the working example, and the broken example with "using". This fix renders the example less perfect for introducing "using" notation, but at least it goes through without errors in my installation (Idris 1.3.0). Is there a better fix which keeps {x:a} up in the "using" clause? --- docs/tutorial/typesfuns.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/tutorial/typesfuns.rst b/docs/tutorial/typesfuns.rst index 7c736f7be7..4651be8c91 100644 --- a/docs/tutorial/typesfuns.rst +++ b/docs/tutorial/typesfuns.rst @@ -574,10 +574,10 @@ appear within the block: .. code-block:: idris - using (x:a, y:a, xs:Vect n a) + using (y:a, xs:Vect n a) data IsElem : a -> Vect n a -> Type where - Here : IsElem x (x :: xs) - There : IsElem x xs -> IsElem x (y :: xs) + Here : {x:a} -> IsElem x (x :: xs) + There : {x:a} -> IsElem x xs -> IsElem x (y :: xs) Note: Declaration Order and ``mutual`` blocks ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~