on 0306e49 help sign in
Idris-dev/impl-paper
21 files
../ Makefilemaking implementation paper depended on local file in some extern directory acmtrans.bstFirst lot of source files and paper acmtrans2m.clsFirst lot of source files and paper comments.styFirst lot of source files and paper compiling.texMissing .tex files conclusions.texProof read for voice/consistency delab.texProof read for voice/consistency elaboration.texProof read for voice/consistency hll.texProof read for voice/consistency impldtp.texPass pattern variable names to match compiler intro.texProof read for voice/consistency jfp.bstSet up .bib jfp1.clsSet up .bib library.bibPass pattern variable names to match compiler library.ltxMore on the core TT literature.bibAdd ElabInfo to pass through elaborator macros.ltxMore on the core TT overview.texMore on elaboration proofstate.texPaper structure; delete useless code syntax.texAdded %hide and %freeze directives typechecking.texProof read for voice/consistency