apparently the metatheory of Idris hasn’t been formalized (or even formulated?) - could be a great Ph.D. project https://groups.google.com/forum/#!msg/idris-lang/grD7ndhy85g/GwHCoO-i_GcJ …
-
-
@edwinbrady *nod*, though i think it's precisely the not-"new"ness of idris that makes it appealing to formalize. afaik we're missing... -
@edwinbrady ...that work, even for the ideas it draws from. or, where it's a subset of existing things, stronger props could be proved here.
End of conversation
New conversation -
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.