From 2364bc7b46bb3ee91be09b53aabaa67150e7a256 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Mar 2022 17:10:12 -0800 Subject: [PATCH] chore: add link to issue --- RELEASES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASES.md b/RELEASES.md index 0999ebe004..bd7f9d49ae 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -189,7 +189,7 @@ def head2 (x : Vector α (n+1)) : α := | a :: as => a -- `::` is `Vector.cons` here ``` -* New notation `.` based on Swift. The namespace is inferred from the expected type. Examples: +* New notation `.` based on Swift. The namespace is inferred from the expected type. See [issue #944](https://github.com/leanprover/lean4/issues/944). Examples: ```lean def f (x : Nat) : Except String Nat := if x > 0 then