git.iko.soy/Idris-dev
on 489ea6f help sign in
history ofimpl-paper/typechecking.tex
all commits
a706b8eProof read for voice/consistencyEdwin Brady 923e19apaper updatesEdwin Brady 3eabe79Added unelaboration definitionEdwin Brady 6a8c4e7Some TODO notes and revisions in the paperEdwin Brady a391979Minor paper changesEdwin Brady d9516eftypos againEdwin Brady ce0bc84Fix typosEdwin Brady a3569e5Some proofreading, filling in some gaps.Edwin Brady 2899286An introductionEdwin Brady 43ffd25Instance tactic explanationEdwin Brady 36abfdaElaborating expressionsEdwin Brady 2b5505dA bit on proof stateEdwin Brady 86c5060An elaboration exampleEdwin Brady 4d2f0feMore on the core TTEdwin Brady 8bf44c2More implementation paperEdwin Brady 0af8a2eWork on implementation paper; tutorial fixesEdwin Brady 8ea902dAdded %hide and %freeze directivesEdwin Brady db7f0c1Paper structure; delete useless codeEdwin Brady