Walking through the format string example in the TDD of Idris2, and trying to do my own version of a format string. Here is what has worked:
data ShowableFmt = NatFmt | CharFmt | DoubleFmt
data CallableFmt = ShwFmt ShowableFmt | StrFmt
data Fmt = CalFmt CallableFmt Fmt | LitFmt String Fmt | EndFmt
FmtType: Fmt -> Type
FmtType fmt = case fmt of
EndFmt => String
LitFmt lit fmt => FmtType fmt
CalFmt callable fmt => case callable of
ShwFmt shwfmt => case shwfmt of
NatFmt => Nat -> FmtType fmt
CharFmt => Char -> FmtType fmt
DoubleFmt => Double -> FmtType fmt
StrFmt => String -> FmtType fmt
So I decide to tidy up a little bit, as we can see -> FmtType fmt
is all over the place. So I do the following, refactoring the repetitive part out and leaving the data type unchanged:
FmtType: Fmt -> Type
FmtType fmt = case fmt of
EndFmt => String
LitFmt lit fmt => FmtType fmt
CalFmt callable fmt => (case callable of
ShwFmt shwfmt => case shwfmt of
NatFmt => Nat
CharFmt => Char
DoubleFmt => Double
StrFmt => String) -> FmtType fmt
Here is the error message:
Error: While processing right hand side of FmtType. Main.case block in case block in FmtType is not accessible in this context.
This kind of surprised me because I thought case
expression is just a normal first class expression like any other expressions. Am I wrong?