on 0222012 help sign in
all commits
c9d2027Use exact name lookup for hidingEdwin Brady 92a4d84Implicit bindings warningsEdwin Brady a7f75c5Merge branch 'feature/deppairparsing' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/deppairparsingEdwin Brady eaf5211Add the ability to define datatypes in ElabDavid Raymond Christiansen be0ff0fAdd 'definable' flag to metavariablesEdwin Brady a009be6Allow setting function flags on instancesEdwin Brady fdfd99eFix behaviour of %hideEdwin Brady fd2501bRenamed `DepPair` to DPairJan de Muijnck-Hughes 5e0e4e9Renamed `UniquePair` to `UPair`.Jan de Muijnck-Hughes 8ed216aRenamed `UPair` to `UniquePair`Jan de Muijnck-Hughes 2951828Idris/AST: minor readability improvementsHeather 8a9ca44Added %auto_implicits directiveEdwin Brady eba5123Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady e3e35a5New rules for name visibilityEdwin Brady faf0b57Merge pull request #2906 from ahmadsalim/feature/uniformstaticanotationJan de Muijnck-Hughes 6042cfeKeep track of names defined in current moduleEdwin Brady 0175376Remove some unnecessary fieldsEdwin Brady be33df4Force sharing of TT sub terms when loading ibcEdwin Brady 8fb4f7fChanged the '[static]' annotation to '%static', for uniformity with the rest of the language.Ahmad Salim Al-Sibahi 9e8930dMerge pull request #2857 from LeifW/watch_files_for_changesEdwin Brady 4d0a065Change "class/instance" keywordsEdwin Brady d77753dMerge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/deppairparsingAhmad Salim Al-Sibahi fd9003bAdded flag to display available logging categories.Jan de Muijnck-Hughes 5f3e700Added new logging category for IBC operations.Jan de Muijnck-Hughes 39a8c78Categorised the Logs.Jan de Muijnck-Hughes 5dc9d1aUpdated logging categories.Jan de Muijnck-Hughes 51e6a29Added a :watch command to the repl to watch for file changesLeif Warner d901c69Initial commit for a category based logger for Idris.Jan de Muijnck-Hughes 9f3675aStore patvar binding types in idris_patdefsShea Levy 06edf43Add implicit lambdas for top level implicitsEdwin Brady c6a8862Add %deprecate directiveEdwin Brady 7bf0ea3Pretty-printer for new nested dependent pair syntaxDavid Raymond Christiansen ce403f6Merge remote-tracking branch 'upstream/master' into wip/tacticalDavid Raymond Christiansen b678d7cChanged scoping rules for unbound implicits.Edwin Brady 30f55ceMerge remote-tracking branch 'upstream/master' into wip/tacticalDavid Raymond Christiansen 1d40dbdMake it possible to disable tactic deprecationDavid Raymond Christiansen 6d7d3bdMerge pull request #2630 from david-christiansen/namesInQQDavid Christiansen 071d34bMake name operations on PTerm quotation-awareDavid Raymond Christiansen 49fae22Add option to desugar nats in REPL outputben-schulz 90bbf06Add deprecation warning for %elimDavid Raymond Christiansen 60b43b4Add raw name quotesDavid Raymond Christiansen 3f31e4eAdd support to keep track of records in IBC filesGuglielmo Fachini 555feb5Add support to keep track of records in IStateGuglielmo Fachini 55ffc21Some display tweaks for explicit argumentsEdwin Brady dfba993Experimental support for console colours on WindowsDavid Raymond Christiansen ffb50e2Insert namespace information to declaration-level %runElabDavid Raymond Christiansen 93761d5Fix source locations for decl syntaxDavid Raymond Christiansen 0655d3dAllow syntax rules at the declaration levelEdwin Brady ab63941Added top-level %runElab supportDavid Raymond Christiansen 7a5392dDisplay tweakEdwin Brady