on 0875310 help sign in
all commits
af0171eProver commands for evaluation and typechecking expressionsDavid Raymond Christiansen 2cff556Another unification fixEdwin Brady c959fb0Unification changesEdwin Brady 5987a95Report errors loading files using semantic highlightingDavid Raymond Christiansen 36527f6Report REPL errors in IDESlave with highlightingDavid Raymond Christiansen 8e6e14aMerge remote-tracking branch 'upstream/master' into semantic-pprintDavid Raymond Christiansen 3051cacMerge pull request #869 from david-christiansen/dynamic-lib-searchEdwin Brady 801aa83More consistency checking on inference constraintsEdwin Brady 71d7de0Some improvements in finding inference constraintsEdwin Brady 3848c07Record partial type inference infoEdwin Brady 36b8f59Improve search for dynamic librariesDavid Raymond Christiansen f6bebd3Proper pretty-printing of dependent pairsDavid Raymond Christiansen a83671eDon't use Curses to look for console width in IDESlaveDavid Raymond Christiansen fa9f021Fix silly name shadowing bug and add new testEdwin Brady 8cde632Merge pull request #846 from david-christiansen/semantic-pprintEdwin Brady e80f871Annotate and colour pairs and () properlyDavid Raymond Christiansen 49df329Make IdeSlave mode follow :consolewidth commandsMelvar Chen 4257d64Automatically detect console widthDavid Raymond Christiansen 106061dUse pretty-printer to display :t for metavarsDavid Raymond Christiansen da24632Render using console widthDavid Raymond Christiansen e46603aMerge remote-tracking branch 'upstream/master' into error-reflectionDavid Raymond Christiansen a2226adMerge remote-tracking branch 'origin/error-reflection' into error-reflectionDavid Raymond Christiansen 8c620dcMerge remote-tracking branch 'upstream/master' into error-reflectionDavid Raymond Christiansen de72eb9More IDESlave semantic highlightingDavid Raymond Christiansen 4d2185bSupport semantic highlighting in IDEslave modeDavid Raymond Christiansen c0cc1ddMerge remote-tracking branch 'upstream/master' into semantic-pprintDavid Raymond Christiansen dc4ce0cReplace the string-slinging show with pretty-printDavid Raymond Christiansen fe3f03fAdded %error_reverse annotationEdwin Brady 5f0c449Colouring support in the proverDavid Raymond Christiansen 13f3c29Basic functioning with new pretty-printerDavid Raymond Christiansen 803194fArgument options (instead of just a Bool for lazy)Edwin Brady b8d7935Hide original errors upon reflective rewriteDavid Raymond Christiansen 0ab30e7Restrict error reflection scope to one argumentDavid Raymond Christiansen e9c9297Make lookupCtxtExact return Maybe instead of ListDavid Raymond Christiansen 1f67398Specific-function error reflection: basic infrastructureDavid Raymond Christiansen d337b5dPerformance/compiler temporary hack: %eraseEdwin Brady ef10474Allow mutually defined instancesEdwin Brady d7b2913A simpler approach to handling name shadowingEdwin Brady 1c51b01EXPERIMENTAL: Disambiguate names in a blockEdwin Brady d82f5feMerge branch 'text-names'Edwin Brady 80a67c5Fix implicit arguments in syntax rulesEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 66ec833Minor memory usage improvementsEdwin Brady a611debFix memory leakEdwin Brady fac49fcSome IBC compressionEdwin Brady dfc3e44Shave a bit more off IBC sizeEdwin Brady 8b7f8adPerformance improvement: name supplyEdwin Brady 0a6fb1fDon't install packages if there are metavariablesEdwin Brady 53b84ecMerge branch 'cabal-library' of https://github.com/puffnfresh/Idris-dev into puffnfresh-cabal-libraryEdwin Brady 5eaf1f5Cut off fruitless proof search earlierEdwin Brady