huohg idris doesn't have DoAndIfThenElse
@Felthry in haskell 2010 this was fixed by making the syntax for 'if' be
if expr1 [;] then expr2 [;] else expr3
with optional semicolons. DoAndIfThenElse is what ghc called its extension to do this before H2010 was finalised. and idris... doesn't have this. so you have to format an 'if' inside a 'do' in the way i strongly dislike
@niss you're... going to have to elaborate on what's going on there because i'm having a lot of trouble parsing the repeated words and it's unclear what it means
-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