git.iko.soy/Idris-dev
on e90d88a help sign in
e90d88aYet more comment cleanupTimo Petteri Sinnemäki 8fcaa82Another wee comment adjustmentTimo Petteri Sinnemäki 751a6eeComment cleanup.Timo Petteri Sinnemäki c78fb14Fixed errors; partially complete default arg subsTimo Petteri Sinnemäki d3eb486First attempt now at substitution to default argsTimo Petteri Sinnemäki b1028f0TacImp script handling to various functions.Timo Petteri Sinnemäki 569a30cMerge branch 'master' of github.com:edwinb/Idris-devTimo Petteri Sinnemäki 63342c7Some helper comments that'll be removed laterTimo Petteri Sinnemäki d763c9cUse postulates for decEq primitive proofsEdwin Brady dfb3982Merge pull request #1006 from david-christiansen/ideslave-optsEdwin Brady 89c89d3Fix "Force" in case tree for new indexed formEdwin Brady 8325cedAllow getting and setting options from IDESlaveDavid Raymond Christiansen 577752bMerge pull request #1002 from david-christiansen/issue/932Edwin Brady a724531Merge pull request #1001 from david-christiansen/doc-arg-namesEdwin Brady 5a4daf5Merge pull request #999 from raichoo/javascriptEdwin Brady 268fd6fMerge pull request #1004 from gabemc/issue/1003Edwin Brady d1e12d5Only show documented arguments in :docDavid Raymond Christiansen 25bbcb0Revert the trifecta change.Gabe McArthur 9607cd8Fixing the build.Gabriel McArthur ae117aaInsert U, UL, and ULL suffixes in CDavid Raymond Christiansen 04e2cd8Stop showing __pi_arg and MNs in docsDavid Raymond Christiansen 7faf4e8Show argument names in :docDavid Raymond Christiansen 9c99a07Add 'covering' function optionEdwin Brady c42ab8bjavascript: skip folding002 testraichoo 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