on 7afa310 help sign in
all commits
edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi 37748ceAdd transformation rules for partial evaluationEdwin Brady 8fc9ffdRefactor REPL command parser, improving error messages at the REPLMichael Maloney aee8f60Parsing a REPL command may now result in a custom error message.Michael Maloney b7010b2New command :pprint for outputting paper/slide bitsDavid Raymond Christiansen 893b980Add :printdef command to show the definition of a pattern-matching operationDavid Raymond Christiansen 783ddc3Invoke external code generatorEdwin Brady 93f407dUse strings for code generatorsEdwin Brady ad81ad3Use a slightly different pretty printer for PDeclsAlyssa Carter 8a48c26Merge branch 'master' into repl-definitionsAlyssa Carter eb241edFixed wrong handling of whitespace between commands and argumentsAhmad Salim Al-Sibahi fb2d914Removed unnecessary backtracking in REPL command parsing making errors harder to understandAhmad Salim Al-Sibahi 5c4f5d2Added an :unlet/:undefine command.Alyssa Carter 2d41378Merge pull request #1363 from bmsherman/parseDefEdwin Brady fc5a9cbFix parser for :def REPL commandbmsherman c1277c8Handling more forms of definition.Alyssa Carter a5e8ca3Changed :let to work with an arbitrary number of `PDecl`s (though only one name at a time for now).Alyssa Carter e260741Preliminary support for a :let command in the replAlyssa Carter d6c5b2bAdd semantic highlighting for postulatesDavid Raymond Christiansen fdb79e6Added warranty information to the Idris Repl.Jan de Muijnck-Hughes ee02ae9Preliminary version of type-directed searchbmsherman 602552eAdd :loadto commandEdwin Brady af99a9dAdd :makelemma command in interactive editingEdwin Brady e16c068Documentation for primitivesDavid Raymond Christiansen 10509f6Add support for :set warnreach.Matus Tejiscak 47304d9Allow the big startup banner to be disabledDavid Raymond Christiansen 6a99256Remove the REPL Info commandPaul Koerbitz 42fb8bfMerge branch 'repl'raichoo 31ca891Parse _|_ as a name in :docDavid Raymond Christiansen 8522683:compile now obeys --codegen flagraichoo 3c8f57c:compile now can take a codegen option (e.g. :compile javascript program.js)raichoo cfbb64fMerge branch 'idrisdoc' of github.com:PhilipRasmussen/Idris-dev into PhilipRasmussen-idrisdocDavid Raymond Christiansen e07c13dAdd :refine (:ref) command for refining a holeEdwin Brady 7bc8bfdAdd REPL commands for who calls whoDavid Raymond Christiansen 877c638IdrisDoc begunPhilip Rasmussen 1921424Add :apropos command to REPLDavid Raymond Christiansen 423b4c4Allow users to disable the auto-solve in the proverDavid Raymond Christiansen 4257d64Automatically detect console widthDavid Raymond Christiansen b8d7935Hide original errors upon reflective rewriteDavid Raymond Christiansen 3b06788Allow querying the registered error handlersDavid Christiansen 5000aebAdd a Cabal libraryBrian McKenna 27a6ec7Merge pull request #640 from david-christiansen/color-theme-default-optionEdwin Brady aadfef8Allow the use of the default foreground colour. Make it the colour of the prompt.David Christiansen 8e974c7Parser cleanup. Removing scaffolding parsers, rewrite PParser and IdeSlave from parsec to Haskell. No more parsec dependenciesAhmad Salim Al-Sibahi 3c32b65Whitespace cleanup.George Leontiev 6adee80Add :apc for adding "proof style" declarationsEdwin Brady b7b55b7Allow hints to be given to proof searchEdwin Brady f869396Add :addmissing REPL commandEdwin Brady abf99a5Add proofsearch tactic, with :ps at the REPLEdwin Brady 7c86659Remove 'catch' round serverEdwin Brady