Hey @edwinbrady, is it known whether the Idris 2 elaborator can be cajoled into doing sudoku?
-
-
Backtracking search during type-checking - oh yes!
-
That is, to a limited degree, what auto implicits give you. Usually (in the common case of resolving interfaces) they are at least under control but who knows what you might be able to get up to.
- 3 more replies
New conversation -
-
-
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.
