Doing rank-n quantification in Idris
I’ve just implemented this in master, allowing implicits in arbitrary scopes, and it’ll be in the next hackage release. It’s not well tested yet though! I have at least tried the following simple examples, and a few others: appShow : Show a => ({b : _} -> Show b => b -> String) -> a … Read more