on f590608 help sign in
all commits
f984657Merge pull request #4093 from melted/export_listsNiklas Larsson 4a3fe0cLinearTypes extension improvementsEdwin Brady bdc6945Add export list to Idris.ErrorNiklas Larsson d4bd8e6Clean up unused imports (#4065)Jason Felice 96a982aAdd do-rewritebe5invis ad13438Check linear types in binders are validEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan f754d9cPurify Idris of "return"David Christiansen f851e54Fix error message for unsuccessful namespace disambiguationBartosz Przygoda d52e4f3Add source location data to PUniverseBartosz Przygoda fdfa04cStore file with constraints + exportEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes b92f7acNew implementation of rewriteEdwin Brady c7bac29Extended syntax for 'with' blocksEdwin Brady 60b43b4Add raw name quotesDavid Raymond Christiansen c9c3bfaSemantic highlighting of implicit fromIntegerDavid Raymond Christiansen bc2915cMerge remote-tracking branch 'upstream/master' into parser-highlightsDavid Raymond Christiansen 5da0d60Faster processing of alternativesEdwin Brady a54852bHighlighting for pairs, lists and sigmasDavid Raymond Christiansen 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen 09f56a7Add compiler highlighting for quoted names in sourceDavid Raymond Christiansen cb1805bAdd local namespace access to ElabDavid Raymond Christiansen 64ab360Tracking and highlighting of metavariablesDavid Raymond Christiansen 7e8e25bMerge branch 'master' into name-highlightsDavid Raymond Christiansen 0419a12Highlight let bindingsDavid Raymond Christiansen f3fef7ePrecise tracking of bindings in do blocksDavid Raymond Christiansen 53e1281Remove PEqMelvar Chen 8984d49Remove PRefl and all references to itMelvar Chen 689e64bHighlight pi and lambda bindersDavid Raymond Christiansen c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen 90127b3High-level if ... then ... else ... expressionDavid Raymond Christiansen 688f324Use any instead of or/map and null/filterNiklas Larsson 8ab1ac6Richer universe error objectsDavid Raymond Christiansen 66c9c38Report universe errors using IDE protocolDavid Raymond Christiansen d6458bbAdd `{n} for quotations of the global name nDavid Raymond Christiansen c3def79Rename Tactical to ElabDavid Raymond Christiansen 933fcbbAdd missing cases to warnDisambDavid Raymond Christiansen d745c2eMerge pull request #1852 from 4e6/repl-module-reloadEdwin Brady 60e4921Relax lower bound on mtlEric Mertens 39c07a7Proper REPL module reloadingDmitry Bushev 2e6b5e0Fix universe checking errorEdwin Brady 73bad9fAdd missing pattern in warnDisambEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady 684a578Completely replace ErrorT with ExceptTbmsherman edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi ce7dff9Error when using empty namespace for disambiguation at REPLDavid Raymond Christiansen 480024cRemove all the handle argumentsDavid Raymond Christiansen 019c98aFix missing function call from 723d972b2David Raymond Christiansen 723d972Fix IDESlave reporting of ProofSearchFailDavid Raymond Christiansen f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen