on 54e4e41 help sign in
all commits
740d82dDisplay normalised types on :t for expressionsEdwin Brady 64df5f6Added WHNF moduleEdwin Brady f48665eFix :dynamic with a lib argNiklas Larsson 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen e3dcb11Fix :search parserEdwin Brady a3407cbDisplay 'Hole' instead of 'Metavariable'Edwin Brady fd5c458Simplify implementation of trimJohannes Griebler 8e550c1Trim trailing whitespace in parseCmdJohannes Griebler 54cd5a6An interactive Elab shellDavid Raymond Christiansen 1d474a2Merge remote-tracking branch 'refs/remotes/upstream/master' into issue/2333David Raymond Christiansen 5542d1cAdd maximum pretty-printer depth option.David Raymond Christiansen 3643346Fixed REPL for `:doc Type` to display documentation rather than an error messageRossMeikleham 4ebafb4Highlight names of simple variable referencesDavid Raymond Christiansen da3a26cAccurate locations for constantsDavid Raymond Christiansen c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen ab9a2bcAdd a :browse command to the REPL and IDE equivalentDavid Raymond Christiansen 5d269e3:exec can take an expression as an argumentEdwin Brady 75f6c2dAdd :core to the REPLDavid Raymond Christiansen 83793a6Add the ability for IDEs to get documentation overviewsDavid Raymond Christiansen 99be9f0Various cleanup of the REPL, mainly with parsing and completionBen Sherman 02a36adAllow :search and :apropos to search packagesEdwin Brady 26da5c7Save index file when installing a packageEdwin Brady b2017d2Pattern variables should be lifted to top levelEdwin Brady 1efff98Ignore leading spaces in REPLMort Yao 647eaedReplace a sequence of <|> with choice.Alexander Shabalin 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