huohg idris doesn't have DoAndIfThenElse
@niss what does this mean?
-F
@Felthry in haskell [and idris which similar syntax] blocks using { ; } can be written following a few rules of indentation. so you can write
do
x <- abc
y <- def
etc
and it'll get desugared to
do { x <- abc; y <- def; etc }.
the problem is if you want to write a conditional inside a block. you may want to write it as
do
if then then
yes yes yes
else
no no no
but under the rules, that becomes
do { if then then yes yes yes; else no no no }
with an unwanted ; before else
