mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
Update CHANGELOG
This commit is contained in:
parent
9b74595de3
commit
d2f54804d7
@ -5,6 +5,8 @@ New in 0.9.10:
|
||||
syntax.
|
||||
* Add 'quoteGoal x by p in e' which makes x equal to p applied to the goal
|
||||
in the scope e
|
||||
* Add !expr notation for implicit binding of intermediate results in monadic/do/etc
|
||||
expressions
|
||||
* Extend Effects package to cope with possibly failing operations, using
|
||||
"if_valid"
|
||||
* At the REPL, "it" now refers to the previous expression
|
||||
|
Loading…
Reference in New Issue
Block a user