../ examples/More sane scoping rules for where/type classes Parameters in the type signature get propagated, indices do not. So you no longer need to pass parameters explicitly if you need them in a where clause, and you no longer need to give explicitly typed helpers …14 years ago MakefileIdiom brackets and dsl notation in tutorial15 years ago classes.texError handling interpreter needs Functor instance (via bishboria)14 years ago conclusions.texAdded note on the empty type and totality checking to the tutorial15 years ago conf.ltxmade TOC in tutorial clickable but still without color15 years ago dsl.texSome re-ordering of the tutorial15 years ago idris-tutorial.pdfUpdate tutorial14 years ago idris-tutorial.texmade TOC in tutorial clickable but still without color15 years ago interp.texMerge branch 'googleclosure' of https://github.com/raichoo/Idris-dev into raichoo-googleclosure14 years ago intro.texMerge branch 'googleclosure' of https://github.com/raichoo/Idris-dev into raichoo-googleclosure14 years ago library.ltxStarted a new tutorial. Don't hold your breath.15 years ago literature.bibFirst complete tutorial draft15 years ago macros.ltxSome more tutorial15 years ago miscellany.texBrief note on implicits in the tutorial14 years ago modules.texMake 'Type' the type of types instead of Sets ...after mailing list discussion14 years ago provisional.texMake 'Type' the type of types instead of Sets ...after mailing list discussion14 years ago starting.texMerge branch 'googleclosure' of https://github.com/raichoo/Idris-dev into raichoo-googleclosure14 years ago syntax.texMake 'Type' the type of types instead of Sets ...after mailing list discussion14 years ago theorems.texMake 'Type' the type of types instead of Sets ...after mailing list discussion14 years ago typesfuns.texSmall library tweaks and documentation update14 years ago views.texMake 'Type' the type of types instead of Sets ...after mailing list discussion14 years ago