mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-14 22:02:07 +03:00
6993c6df6b
helps with readability since these, especially named-IPi, come up a lot didn't change everything that could need it like PiInfo or BindMode PiInfo rarely has DefImplicit (so far) and BindMode hasn't come up a lot (so far) reduced indentation for TTImp Show implementation |
||
|---|---|---|
| .. | ||
| expected | ||
| Hole.yaff | ||
| input | ||
| run | ||