git.iko.soy/Idris-dev
on dd1665b help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
d337b5dPerformance/compiler temporary hack: %eraseEdwin Brady 567b1beMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady d7b2913A simpler approach to handling name shadowingEdwin Brady 970c833Merge pull request #782 from jfdm/feature/pkg-check-onlyEdwin Brady 1c51b01EXPERIMENTAL: Disambiguate names in a blockEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady a611debFix memory leakEdwin Brady fdbee50Command line option improvements.Jan de Muijnck-Hughes fac49fcSome IBC compressionEdwin Brady 8b7f8adPerformance improvement: name supplyEdwin Brady 3b06788Allow querying the registered error handlersDavid Christiansen 8f95300Allow functions to be declared as error handlersDavid Christiansen d7f4e11Induction now works on types with parametersAhmad Salim Al-Sibahi 53b84ecMerge branch 'cabal-library' of https://github.com/puffnfresh/Idris-dev into puffnfresh-cabal-libraryEdwin Brady 5e7fc5dAdd 'byReflection' tacticEdwin Brady 67da31aMerge branch 'master' into cabal-libraryBrian McKenna dccddd2Merge branch 'forceability-cleanup-squashed' of https://github.com/ziman/idris into ziman-forceability-cleanup-squashedEdwin Brady 2e570a3Merge branch 'default-superclass-instances' of https://github.com/puffnfresh/Idris-dev into puffnfresh-default-superclass-instancesEdwin Brady 99beed8Default superclass intancesBrian McKenna 65c301cRecursive constructor disjointness + cleanupMatus Tejiscak 2dc07faInduction on nat workingAhmad Salim Al-Sibahi 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 a0b21e3AbsSyntaxTree `showName` should use `showCG`, not `show`Brian McKenna 0f97368Merge branch 'master' into cabal-libraryBrian McKenna 5000aebAdd a Cabal libraryBrian McKenna 027bd15Merge pull request #675 from cgswords/masterEdwin Brady 725587fFixed testing failures I accidentally introduced when showing a better naming for machine generated names (so that I could better debug)Ahmad Salim Al-Sibahi ec3daa4Make sure deferred definitions get totality checkedEdwin Brady 386753dAdded a --nobanner flag to supress the banner.cswords 9a89a8dEliminators working for some type - still experimental. Will create a way to make them work with the elim type classAhmad Salim Al-Sibahi a10e866Added data optionsAhmad Salim Al-Sibahi ddac624Add --nobasepkgs flagEdwin Brady 90eb6a2Library changes: Please read details below!Edwin Brady 543cd7eStrictness improvementsEdwin 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 23772e9Remove "CaseSplit" constructor and implementation which could never be called (the REPLParser uses CaseSplitAt). Furhermore, we no longer need to export "split" from CaseSplit.hsHannes Mehnert 16eee46Fix case split bug on complex nested patternsEdwin Brady 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 53ce3ccProof search now also tries recursive callsEdwin Brady 5d2d5a7Failed proofsearch branch creates new metavariableEdwin Brady abf99a5Add proofsearch tactic, with :ps at the REPLEdwin Brady f34f0afBetter display of metavariable types in :tEdwin Brady