on ca30292 help sign in
all commits
f707c76Merge remote-tracking branch 'upstream/master' into error-reflectionDavid Raymond Christiansen 3e401fbImprove error pretty-printingDavid Raymond Christiansen 992acb4Fix regression with data declarations in whereEdwin Brady 7437ebePrepared data structure of FC for spanning, and added the span of the last token parsed to IdrisAhmad Salim Al-Sibahi a7e6550Merge pull request #962 from david-christiansen/markdown-docsEdwin Brady d910c2cUse Markdown to represent docstringsDavid Raymond Christiansen 423b4c4Allow users to disable the auto-solve in the proverDavid Raymond Christiansen be57f4aFix unbound implicit rulesEdwin Brady c1ef938New syntax for documentation commentsDavid Raymond Christiansen c37de47Propagate parameters to recordsEdwin Brady 7b32c97No need to export primitives as metavariablesEdwin Brady 2df0a7fStore metavariables in ibc filesEdwin Brady 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