on cb005bc help sign in
all commits
e4cf620Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady d745c2eMerge pull request #1852 from 4e6/repl-module-reloadEdwin Brady 8096500Add %used pragmaEdwin Brady f6df58cMerge branch 'master' of github.com:idris-lang/Idris-dev into new_ffiEdwin Brady d5377beNew language-dependent FFIEdwin Brady 60e4921Relax lower bound on mtlEric Mertens 39c07a7Proper REPL module reloadingDmitry Bushev 21ccbe8Parse 'with' arguments in pattern modeEdwin Brady 6b803b7Allow documentation for modulesDavid Raymond Christiansen f936366Merge pull request #1817 from bmsherman/replEdwin Brady 99be9f0Various cleanup of the REPL, mainly with parsing and completionBen Sherman 7c34217Allow class constraints to be namedEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady 684a578Completely replace ErrorT with ExceptTbmsherman 7b5f4aaFix visibility of imported thingsEdwin Brady 9d804b5Optimize custom syntax rulesAlexander Shabalin e90316aSupport type errors in docstringsDavid Raymond Christiansen 6e74e33Fix for pattern vars in transformsEdwin Brady 37eae55Factor `addSyntax` out of `syntaxDecl` parserAlyssa Carter 5dcb90eAdded parser FIXMEs to the issue tracker.Jan de Muijnck-Hughes 37292e1Save terms in docstringsDavid Raymond Christiansen 93f407dUse strings for code generatorsEdwin Brady 788f800Record import paths in ibcEdwin Brady 480024cRemove all the handle argumentsDavid Raymond Christiansen 1add7b7provide a Handle for IdeSlave, used to read from and write to (instead of hardcoded stdin/stdout) also send protocol-version message when the client connects also accept a single client connection when --ideslave-socket is provided (I don't see any reason to have multiple clients at all!)Hannes Mehnert 382542aAdd %no_implicit directiveEdwin Brady 72cddc6Generate legal names for infix op lemmasDavid Raymond Christiansen c201192Bring erasure info to the case tree builder.Matus Tejiscak e5bc47eDistinguish postulate providers and type providers at use siteDavid Raymond Christiansen 21124c3Merge remote-tracking branch 'upstream/master' into cantResolveAltsbmsherman 9907240Add new Err constructor to disambiguate the CantResolveAlts constructor.bmsherman 5c4ee75Make load to line work with mutual blocksEdwin Brady 94fc13cIDESlave support for :loadtoDavid Raymond Christiansen 602552eAdd :loadto commandEdwin Brady e1f7597Merge pull request #1204 from david-christiansen/totality-warningEdwin Brady f979614Merge pull request #1208 from david-christiansen/primitive-docsDavid Christiansen e16c068Documentation for primitivesDavid Raymond Christiansen aabd0a9Allow %name to take an infix name as an argument.David Raymond Christiansen 7143962Make totality a warning until compilingDavid Raymond Christiansen 0663f4dMerge pull request #1183 from pminten/ppoptEdwin Brady 5e3c248Change impl argument to a pretty printing opt recordPeter Minten 104635bPrevent double-printing some FCsDavid Raymond Christiansen da45e7dFollow IDESlave protocol when import not foundDavid Raymond Christiansen a3fa5a4Bring module loading into Idris monadDavid Raymond Christiansen 4035b5dAdd a field for parameter docstrings in the PClass constructor of PDecl'Paul Koerbitz 08fbb4eSimplified some lookaheads and grammar rules for lambda expressions and other internal expressions.Ahmad Salim Al-Sibahi 6857d73Merge pull request #1035 from puffnfresh/bug/parser-nocolourEdwin Brady 6aeacd8Make parsing respect the nocolour flagBrian McKenna bfc3c3eMerge branch 'master' of github.com:edwinb/Idris-dev into default-arg-substTimo Petteri Sinnemäki c78fb14Fixed errors; partially complete default arg subsTimo Petteri Sinnemäki