I often read on the Internet - and I realise that I should know by now that it's not a good place to read things - that Idris isn't Turing Complete and can't be because it's dependently typed. I think I can guess where this idea comes from, but, in case of any doubt, it's Turing Complete. Of course it's Turing Complete. For goodness sake...
=> More informations about this toot | View the thread | More toots from edwinb@types.pl
text/geminiThis content has been proxied by September (3851b).