git.iko.soy/Idris-dev
on 0690def help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
d337b5dPerformance/compiler temporary hack: %eraseEdwin Brady ef10474Allow mutually defined instancesEdwin Brady d7b2913A simpler approach to handling name shadowingEdwin Brady 1c51b01EXPERIMENTAL: Disambiguate names in a blockEdwin Brady d82f5feMerge branch 'text-names'Edwin Brady 80a67c5Fix implicit arguments in syntax rulesEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 66ec833Minor memory usage improvementsEdwin Brady a611debFix memory leakEdwin Brady fac49fcSome IBC compressionEdwin Brady dfc3e44Shave a bit more off IBC sizeEdwin Brady 8b7f8adPerformance improvement: name supplyEdwin Brady 0a6fb1fDon't install packages if there are metavariablesEdwin Brady 53b84ecMerge branch 'cabal-library' of https://github.com/puffnfresh/Idris-dev into puffnfresh-cabal-libraryEdwin Brady 5eaf1f5Cut off fruitless proof search earlierEdwin Brady 67da31aMerge branch 'master' into cabal-libraryBrian McKenna 2aab37fMerge pull request #731 from hannesm/report-column-on-warningEdwin Brady 8c93763Careful when unifying explicit argumentsEdwin Brady cbe9965on error, report the column, as well as the line number in the ideslave mode.Hannes Mehnert 99beed8Default superclass intancesBrian McKenna 4a0eba1Add %name directive for naming hints in editing.Edwin Brady 7b8f3b4Merge branch 'feature/eliminators' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/eliminatorsEdwin Brady 232a592Replace partial `showDeclImp` function with total `dumpDecl`Brian McKenna 0f97368Merge branch 'master' into cabal-libraryBrian McKenna 5000aebAdd a Cabal libraryBrian McKenna 027bd15Merge pull request #675 from cgswords/masterEdwin Brady ec3daa4Make sure deferred definitions get totality checkedEdwin Brady 386753dAdded a --nobanner flag to supress the banner.cswords b3bf956When specialising, reduce more namesEdwin Brady 9a89a8dEliminators working for some type - still experimental. Will create a way to make them work with the elim type classAhmad Salim Al-Sibahi 77b1fafSwitch on 'elabPE'Edwin Brady a10e866Added data optionsAhmad Salim Al-Sibahi 0e3d87eMore flexible type class instances (on functions)Edwin Brady b1537b9Report errors directly, instead of parsing the string given to ihputStrLnHannes Mehnert 8a2804dUse _ if all alternatives are unmatchableEdwin Brady 5521f95Don't allow matching on functions without justificationEdwin Brady 9c9b38bsend log over the wire if in ideslave mode doesn't capture the Debug.Trace usage in Core (with log level >= 5) yet, unfortunatelyHannes Mehnert 01078f2Merge pull request #641 from ahmadsalim/feature/metavarprooffixEdwin Brady 1e6c727Disallow proving of top-level declarations and other meta-variables, fixes idris-lang/Idris-dev#46Ahmad Salim Al-Sibahi 8e974c7Parser cleanup. Removing scaffolding parsers, rewrite PParser and IdeSlave from parsec to Haskell. No more parsec dependenciesAhmad Salim Al-Sibahi 8b91e60Make --ideslave imply --nocolourDavid Christiansen 8531634Set up more partial evaluation machineryEdwin Brady 6b3457aName resolution should respect %hideEdwin Brady 3c32b65Whitespace cleanup.George Leontiev 53ce3ccProof search now also tries recursive callsEdwin Brady f34f0afBetter display of metavariable types in :tEdwin Brady 46256abAdd ':addclause' command at the REPLEdwin Brady d20f35cAdd --client optionEdwin Brady 66f4f9eExtend split/splitOnLine to cope with 'where/with'Edwin Brady 8c19e30Record internal name of 'with' functionsEdwin Brady