git.iko.soy/Idris-dev
on 10ea548 help sign in
Idris-dev/tutorial
1 folder, 18 files
../ examples/Note on cumulativity in tutorial MakefileBinary adder example classes.texDebraced tutorial conclusions.texFirst complete tutorial draft idris-tutorial.pdfintros tactic; some library tinkering idris-tutorial.texFirst complete tutorial draft interp.texSome prelude shuffling intro.texFormatting library.ltxStarted a new tutorial. Don't hold your breath. literature.bibFirst complete tutorial draft macros.ltxSome more tutorial miscellany.texintros tactic; some library tinkering modules.texDebraced tutorial provisional.texAdded Cast to the prelude, and defined casts between primitives starting.texFormatting syntax.texTinkered with syntax rules section in tutorial theorems.texintros tactic; some library tinkering typesfuns.texChange 'data' and where syntax so that they don't need '|' This breaks old code - instead of views.texChange 'data' and where syntax so that they don't need '|' This breaks old code - instead of