max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add link to issue

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-10 17:10:12 -08:00
parent 002412e9d0
commit 2364bc7b46
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
RELEASES.md
View file

@ -189,7 +189,7 @@ def head2 (x : Vector α (n+1)) : α :=
| a :: as => a -- `::` is `Vector.cons` here
```
* New notation `.<identifier>` based on Swift. The namespace is inferred from the expected type. Examples:
* New notation `.<identifier>` 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