git.iko.soy/Idris-dev
on 0939fb5 help sign in
0939fb5Progress: IdrisDoc is now able to generate output to the necessary files. Actual structured content is TODOPhilip Rasmussen 5401872Merge remote-tracking branch 'upstream/master' into idrisdocPhilip Rasmussen 7762a35Package paths may now be in other locations than current directoryPhilip Rasmussen 13d63e3Rewrote implementation so far to be much smarterPhilip Rasmussen 6b3bbe7NameTrie added to create map of names for easy lookupPhilip Rasmussen 39ac157Added IdrisDoc hooks from the command line.Philip Rasmussen d4abcb8Added IdrisDoc hooks from the command line.Philip Rasmussen e21b167Tiny tidying upPhilip Rasmussen 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 9b1746cMerge remote-tracking branch 'upstream/master' into idrisdocPhilip Rasmussen 77eca9cChanged IdrisDoc interface, updated command descriptions.Philip Rasmussen 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 155e306Fixed IdrisDoc errors and added REPL :help descriptionsPhilip Rasmussen 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 877c638IdrisDoc begunPhilip Rasmussen 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