mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
239c8caffa
It is, in some sense, a proof search, and this means that auto proof search can now solve things which require type class resolution. One side-effect is that type class resolution will now only solve holes which actually are type classes! So this may break code which was abusing the type class resolution mechanism - such code can most likely be rewritten to do proof search. |
||
|---|---|---|
| .. | ||
| expected | ||
| input | ||
| interactive009.idr | ||
| run | ||