From e1f4fbba836295de59e6cef5463220eb8bb8a7f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Tue, 23 Jan 2024 19:37:49 +0900 Subject: [PATCH] Update docs/source/reference/operators.rst --- docs/source/reference/operators.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/source/reference/operators.rst b/docs/source/reference/operators.rst index 0ccafa44e..22bc2d233 100644 --- a/docs/source/reference/operators.rst +++ b/docs/source/reference/operators.rst @@ -240,8 +240,8 @@ Typebind Operators ================== In dependently-typed programming, we have the ability define constructors which -first argument is a type and the second is a lambda using the first argument -as it's type. A typical example of this is the dependent linear arrow: +first argument is a type and the second is a type indexed over the first argument. +A typical example of this is the dependent linear arrow: .. code-block:: idris