git.iko.soy/Idris-dev
on e8ea34b help sign in
e8ea34bMoved pinfo back into the where blockTimo Petteri Sinnemäki 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