git.iko.soy/Idris-dev
on 155e306 help sign in
155e306Fixed IdrisDoc errors and added REPL :help descriptionsPhilip Rasmussen 877c638IdrisDoc begunPhilip Rasmussen 9c99a07Add 'covering' function optionEdwin Brady 7cea995Add tests for tutorial examplesEdwin Brady 678fc86Finish guardedness checkEdwin Brady 303e100Fix reading of line/column on parse errorsEdwin Brady 5232002Make names accessible before building case splitEdwin Brady 7af5df9isFnName should look for exact namesEdwin Brady c06badbRequire content in tactic/proof blocksEdwin Brady b0720b0Change guardedness check for new-style coinductionEdwin Brady 71a968cChange reduction rules for coinductive definitionsEdwin Brady 88aa6d1Support mixed induction/coinduction with Inf typeEdwin Brady 85852c2Fix line number on invocation of :eEdwin Brady da93e25Merge pull request #990 from david-christiansen/unifier-contextEdwin Brady f490d9fFix testDavid Raymond Christiansen fc949b9Re-enable function arg error reflectionDavid Raymond Christiansen 57c3ffcAdd application context to all error messagesDavid Raymond Christiansen 60f7427Merge remote-tracking branch 'upstream/master' into unifier-contextDavid Raymond Christiansen 0fc0cdcMerge pull request #991 from jfdm/doc/effectsEdwin Brady a706a7aMerge pull request #989 from david-christiansen/docsEdwin Brady 3cef609Annotate 'Lazy' with reason for lazinessEdwin Brady 82c94b3Remove some commented-out codeDavid Raymond Christiansen 1290495Initial documentation efforts for effectsJan de Muijnck-Hughes f01873fAdd stack of elaboration context to ElaboratingArgDavid Raymond Christiansen 1d867e5More docstringsDavid Raymond Christiansen 7f3d436Remove some commented out codeEdwin Brady e579ceeDocs for decEqDavid Raymond Christiansen 77701e1Save pattern definitions/missing casesEdwin Brady 3bb3273Remember to save deferred definition types in IBCEdwin Brady c5cb67cFix simple applicationEdwin Brady 45a0addUpdate for new unification error messagesDavid Raymond Christiansen 465d169Temporarily change back to UN to avoid strange errorsDavid Raymond Christiansen be0bf4cTemporarily remove function argument error reflectionDavid Raymond Christiansen f569155Update test for more informative error messagesDavid Raymond Christiansen fb3f7f0Use At to hold FCsDavid Raymond Christiansen 5cee305Update CHANGELOGDavid Raymond Christiansen aed179cTrack the providence of unification errorsDavid Raymond Christiansen ff742feActually track applications in the elaborator wrt unification failsDavid Raymond Christiansen b38bc03Add basic elaboration context tracking to unificationDavid Raymond Christiansen daafe34Merge pull request #980 from david-christiansen/jedesah-vect_lengthEdwin Brady ca564fdRemove java tests from travisEdwin Brady e9ef380Support text formatting in docstringsDavid Raymond Christiansen e7c5cb2Add a note to Vect.length about when to use itDavid Raymond Christiansen 1b81d69Merge pull request #985 from david-christiansen/keyword-highlightEdwin Brady 99ab467Merge pull request #984 from david-christiansen/fin-add-mulEdwin Brady 79000baMerge pull request #981 from david-christiansen/docsEdwin Brady ca30292Merge pull request #979 from david-christiansen/feature/aproposEdwin Brady 24bfcd8Merge pull request #977 from jedesah/vect_lengthEdwin Brady 15aebc9Add highlighting for keywords in interpreter outputDavid Raymond Christiansen 021e090Addition and multiplication of FinDavid Raymond Christiansen