mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 05:01:34 +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 |
||
---|---|---|
.. | ||
basic001 | ||
basic002 | ||
basic003 | ||
basic004 | ||
basic005 | ||
basic006 | ||
coverage001 | ||
coverage002 | ||
dot001 | ||
eta001 | ||
eta002 | ||
lazy001 | ||
nest001 | ||
nest002 | ||
perf001 | ||
perf002 | ||
perf003 | ||
qtt001 | ||
qtt003 | ||
record001 | ||
record002 | ||
record003 | ||
total001 | ||
total002 | ||
total003 |