From 46a2dc1c1f7b195a093715a4146566a43cba027e Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Thu, 22 Jun 2023 17:21:08 +0300 Subject: [PATCH] [ doc, tiny ] Correct wrong directive for unbound implicits turning off --- docs/source/faq/faq.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/faq/faq.rst b/docs/source/faq/faq.rst index b24a36e5e..f25d008be 100644 --- a/docs/source/faq/faq.rst +++ b/docs/source/faq/faq.rst @@ -269,7 +269,7 @@ directive: .. code-block:: idris - %auto_implicits off + %unbound_implicits off In this case, you can bind ``n`` and ``m`` as implicits, but not ``ty``, as follows: