on 3d59246 help sign in
3d59246Normalise thunk contents when returning from executorDavid Raymond Christiansen ce414b8Regression test for infinite regress in executorDavid Raymond Christiansen 25c1352Support for typed laziness in executorDavid Raymond Christiansen 7d09d05Merge pull request #1016 from SimonJF/rts-deadlock-fixEdwin Brady a93acd6Merge pull request #1014 from david-christiansen/doc-type-ideslaveEdwin Brady 1569aa9Merge pull request #1012 from david-christiansen/issue/949Edwin Brady 8f5e40fMerge pull request #1009 from jedesah/list_splitAtEdwin Brady aa91121Fix deadlock in RTS when using allocation in native codeSimon Fowler f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen dd20facAdd semantic highlighting info for metavariablesDavid Raymond Christiansen d763c9cUse postulates for decEq primitive proofsEdwin Brady 06fbec1Add name of arguments in type declaration for proper documentationJean-Remi Desjardins dfb3982Merge pull request #1006 from david-christiansen/ideslave-optsEdwin Brady 89c89d3Fix "Force" in case tree for new indexed formEdwin Brady e058452Add splitAt function for ListJean-Remi Desjardins 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