Adowrath

@slideon The diff percentage says "How many % of the changes made in this PR are covered?". Codecov uses many metrics to compare coverage, and that's one of them. It's...

Right now, https://github.com/idris-lang/Idris2/commit/f76c4c4307 "fixes" this by forcing the maximum visibility to apply. This makes any combination of the three modifiers on either of the forward or actual declaration result in...

> If only we had a gadget that allowed us to express that something is the default without conflating it with the default value it takes. 🤔 > > http://gallais.github.io/blog/ceci-pas-default...

~~Fixed the missing EOLs, `fend` should run through now @Bodigrim.~~ Ugh, I should actually `git add` before amending, sorry. **Now** it should run through.