| .. |
| Elab | Fix lambda multiplicity check | 6 years ago |
| Interactive | newtype optimisation | 6 years ago |
| BindImplicits.idr | Add default implicit arguments | 6 years ago |
| Elab.idr | Prioritise resolution of delayed elaborators | 6 years ago |
| Impossible.idr | Take environment into account in coverage check | 6 years ago |
| Parser.idr | bugfix: actually include keyword "default" for default implict record type arguments | 6 years ago |
| PartialEval.idr | Complete specialised definitions | 6 years ago |
| ProcessData.idr | Erase the World, with care | 6 years ago |
| ProcessDecls.idr | Only record fields should be in a new namespace | 6 years ago |
| ProcessDef.idr | Don't fully normalise LHS | 6 years ago |
| ProcessParams.idr | Fix where under multiple cases | 6 years ago |
| ProcessRecord.idr | Bugfix: differentiate between implicit and explicit arguments in the return type of the constructor | 6 years ago |
| ProcessType.idr | Syntax for flagging arguments to specialise | 6 years ago |
| Reflect.idr | Use a data type for dotting reason | 6 years ago |
| TTImp.idr | Refactor to allow supporting implicit and rit annotations on records (without adding syntax for them) | 6 years ago |
| Unelab.idr | Add default implicit arguments | 6 years ago |
| Utils.idr | Only record fields should be in a new namespace | 6 years ago |
| WithClause.idr | Add default implicit arguments | 6 years ago |