git.iko.soy/Idris-dev
on aeb032a help sign in
history ofsrc/Idris/TypeSearch.hs
all commits
4878fe4Allow upper case letter in package name and only normalize for equality and on diskVincent Hanquez f732f9dIntroduce a PkgName abstraction to represent package name instead of StringVincent Hanquez 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice 89dd6aeCheck linearity of functionsEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) 06d9db6Use interface instead class or type class in documentations (#3379)(λ _ λ) c3f0755replace code level class symbol with inferfacezjhmale fdfa04cStore file with constraints + exportEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes 536372fRename Lazy' => DelayedEdwin Brady 9297ae4Allow 'data' declarations in interfacesEdwin Brady a7e434aAllow Elab scripts to register type class instancesDavid Raymond Christiansen 268296fHighlight the names in type declarationsDavid Raymond Christiansen f987aecAdd info field to AppEdwin Brady d89af9ccleaned up redundant 'if'JP Smith 5f0dbd7clarify failing searchesJP Smith 15737d9Trickiness with implicits in dependent classesEdwin Brady 426d052Add provenance flag to unification errorsEdwin Brady 9790b8fIgnore lazy type modifiers in :searchBen Sherman b85b2ebRename ideslave to ide-modeDavid Raymond Christiansen c729d2fSupport scoped type class constraintsEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady 140cfe2Small changes and documentation update to :searchBen Sherman 02a36adAllow :search and :apropos to search packagesEdwin Brady 26da5c7Save index file when installing a packageEdwin Brady 00f1cd5Use ExceptT instead of ErrorTbmsherman 37292e1Save terms in docstringsDavid Raymond Christiansen 7ce4d90Add annotations for :search result classificationbmsherman 185f808Fix logical error in :search's unification resolutionbmsherman aa98ab1Try symmetry of equality in :searchbmsherman 886bac0Refactor :search to remove code duplication and name shadowingbmsherman 7e7368dStore kind in Pi bindersEdwin Brady 480024cRemove all the handle argumentsDavid Raymond Christiansen 1add7b7provide a Handle for IdeSlave, used to read from and write to (instead of hardcoded stdin/stdout) also send protocol-version message when the client connects also accept a single client connection when --ideslave-socket is provided (I don't see any reason to have multiple clients at all!)Hannes Mehnert c72d0f4Split elaborator into multiple source filesEdwin Brady 7d95becMake type search work in the proverDavid Raymond Christiansen 78b2923Correctly count applications of variables in :searchbmsherman d7f6164Ignore believe_me in :search since its type is a lie!bmsherman e1ba862Find best matching types first in :search with a priority queue.bmsherman d19891cDiscover typeclass introduction/elimination in :searchbmsherman eec9953In :search, check injectivity to prevent erroneous resultsbmsherman e1ef65dUse a priority queue to improve performance when matching types in :searchbmsherman 114a307Prevent possibility of unbounded computation in :searchbmsherman f91051aIgnore default class methods in :searchbmsherman 852301dImprovements to :search, primarily in handling typeclassesbmsherman