git.iko.soy/Idris-dev
on 0222012 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
92a4d84Implicit bindings warningsEdwin Brady 4c9b9efauto_implicit fixEdwin Brady c1decafFix implicit name bindings in interfacesEdwin Brady cda5443Insert _ for implicit methodsEdwin Brady 6520891Unify pattern and implicit name binding rulesEdwin Brady 76c46bbMore flexible holesEdwin Brady be0ff0fAdd 'definable' flag to metavariablesEdwin Brady a009be6Allow setting function flags on instancesEdwin Brady fdfd99eFix behaviour of %hideEdwin Brady 2951828Idris/AST: minor readability improvementsHeather 8a9ca44Added %auto_implicits directiveEdwin Brady e3e35a5New rules for name visibilityEdwin Brady 6042cfeKeep track of names defined in current moduleEdwin Brady 0175376Remove some unnecessary fieldsEdwin Brady f7a9c28Tweak implicit name rulesEdwin Brady be33df4Force sharing of TT sub terms when loading ibcEdwin Brady 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 d901c69Initial commit for a category based logger for Idris.Jan de Muijnck-Hughes 06edf43Add implicit lambdas for top level implicitsEdwin Brady c6a8862Add %deprecate directiveEdwin Brady da914afConsistency of implicit/pattern name binding rulesEdwin Brady 83f0af1Display expected type of RHS in error messagesEdwin Brady f1ff8fbMerge pull request #2634 from david-christiansen/namesInQQDavid Christiansen 92c1959Respect quotation when expanding parametersDavid 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 2f9d287Implicit fixEdwin Brady 4b3c477Merge pull request #2569 from GuglielmoS/fix/master/2241David Christiansen 0fbfeabImprove pruning of alternativesEdwin Brady 555feb5Add support to keep track of records in IStateGuglielmo Fachini b573bf0Improve addImpl under PHiddenEdwin Brady 7095d6cProof search should only use user visible namesEdwin Brady 740d82dDisplay normalised types on :t for expressionsEdwin Brady c9c3bfaSemantic highlighting of implicit fromIntegerDavid Raymond Christiansen bc2915cMerge remote-tracking branch 'upstream/master' into parser-highlightsDavid Raymond Christiansen 5da0d60Faster processing of alternativesEdwin Brady a54852bHighlighting for pairs, lists and sigmasDavid Raymond Christiansen 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen ac68541Dump highlighting infoDavid Raymond Christiansen 823be86Highlight postulates and their definitionsDavid Raymond Christiansen 202c913Logging levels must be explicitly mentioned.Jan de Muijnck-Hughes 63806e5Mark free implicits as dottedDavid Raymond Christiansen 6bf22eeMerge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 34f516dCanonicalize paths in internalappDavid Raymond Christiansen 9056a4aMerge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen bfacfbcBetter partial evaluation of polymorphic HOFsEdwin Brady cb1805bAdd local namespace access to ElabDavid Raymond Christiansen