on a427f21 help sign in
all commits
00f1cd5Use ExceptT instead of ErrorTbmsherman 941ba6eImplemented @-patternsEdwin Brady 7b5f4aaFix visibility of imported thingsEdwin Brady 58dd2b5Move Pair/Sigma into Builtins namespaceEdwin Brady 75c7597Improve delaboration and pretty-printing for caseDavid Raymond Christiansen f1e161dA new primitive tactic for getting source locationsDavid Raymond Christiansen 1437f86Fix typo in commentDavid Raymond Christiansen b2017d2Pattern variables should be lifted to top levelEdwin Brady 4130476Just store sorted list of syntax rulesAlexander Shabalin 9d804b5Optimize custom syntax rulesAlexander Shabalin ab2a29fMerge pull request #1658 from david-christiansen/todo-removalEdwin Brady cdff1dbMerge pull request #1659 from edwinb/partial-evalEdwin Brady 8e6b636Optimisation optionsEdwin Brady 30580dbRemoval of minor TODOsDavid Raymond Christiansen 03f6913Partially evaluate type class dictionariesEdwin Brady e90316aSupport type errors in docstringsDavid Raymond Christiansen e890280Merge pull request #1619 from ahmadsalim/feature/renamevoidEdwin Brady 37eae55Factor `addSyntax` out of `syntaxDecl` parserAlyssa Carter d6981dcRenamed VoidElim to void in order to ensure further consistencyAhmad Salim Al-Sibahi edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi 869e6caMerge branch 'master' of git://github.com/idris-lang/Idris-dev into partial-evalEdwin Brady 37748ceAdd transformation rules for partial evaluationEdwin Brady 7383b1cSupport nested quasiquotationDavid Raymond Christiansen a57302cMerge pull request #1563 from david-christiansen/comments-on-ptermDavid Christiansen a5c9dc5Add more docs to PTermDavid Raymond Christiansen 37292e1Save terms in docstringsDavid Raymond Christiansen 840c2ccMerge pull request #1556 from Helkafen/masterDavid Christiansen 4fd6bc6Allow REPL to run on another port (flag --port)Sebastian de Bellefon fe569c4Finished making standard library naming consistentAhmad Salim Al-Sibahi 6faa1abRenaming of built-in datatypes works finallyAhmad Salim Al-Sibahi f0ed9e9First renaming attemptAhmad Salim Al-Sibahi b7010b2New command :pprint for outputting paper/slide bitsDavid Raymond Christiansen 4d85599Improve pretty-printing of "let"David Raymond Christiansen ba0b525Pretty-printing of implicit args to (=)David Raymond Christiansen 7ce4d90Add annotations for :search result classificationbmsherman 893b980Add :printdef command to show the definition of a pattern-matching operationDavid Raymond Christiansen ce7dff9Error when using empty namespace for disambiguation at REPLDavid Raymond Christiansen 7e7368dStore kind in Pi bindersEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady ddced5cStore parameters in function typesEdwin Brady 93f407dUse strings for code generatorsEdwin Brady 3d1a728Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 788f800Record import paths in ibcEdwin Brady ecea9adMerge branch 'master' into repl-definitionsAlyssa Carter d947282Merge pull request #1452 from hannesm/ideslave-socketDavid Christiansen 480024cRemove all the handle argumentsDavid Raymond Christiansen 2418336Save some allocations in updateSolvedEdwin Brady ab36099Use a zipper-like proof stateEdwin Brady 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 be0a480provide a new option, --ideslave-socket, for an ideslave listening on a socketHannes Mehnert