git.iko.soy/Idris-dev
on d9516ef help sign in
history oftutorial/miscellany.tex
all commits
0af8a2eWork on implementation paper; tutorial fixesEdwin Brady 891b52a%obj should be %link in tutorialEdwin Brady 486b176Some re-ordering of the tutorialEdwin Brady 34331d9Document auto implicitsEdwin Brady 2ce525eintros tactic; some library tinkeringEdwin Brady 0b9cab2Note on cumulativity in tutorialEdwin Brady 2e9fcd4Remove semicolons in tutorialEdwin Brady e24955aNote on where scoping and types in tutorialEdwin Brady 310ca03First complete tutorial draftEdwin Brady ebf9100Binary adder exampleEdwin Brady c6c3901Added well-typed interpreter section to tutorialEdwin Brady 8fbef42Started a new tutorial. Don't hold your breath.Edwin Brady