impl-paper/Some effort at reporting line numbers of errors (top level of decl only)15 years ago lib/Improved where; implicit arguments now expanded during elaboration15 years ago src/:r and :e at the REPL.15 years ago LICENSEFix LICENSE15 years ago MakefileSugar for dependent pairs15 years ago READMEFirst commit15 years ago interp.idr:r and :e at the REPL.15 years ago miniidris.cabalBeginning theorem prover interface15 years ago