Any Idris folks can help me with this question? I'm trying to do induction on a single constructor argument, but Idris isn't convinced that my inductive definition is total.https://stackoverflow.com/q/59777677/525872?stw=2 …
-
-
The salient feature seems to be that we only have a single constructor. If there were two constructors then this trick wouldn't work. So it makes sense to me that Idris might struggle with this kind of special case. But I can't figure out how to work around it.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.