git.iko.soy/Idris-dev
on bf4e535 help sign in
history ofsrc/Idris/Elab/Data.hs
all commits
cc9895dMerge branch 'improve-universe-solver' of https://github.com/ozgurakgun/Idris-dev into ozgurakgun-improve-universe-solverEdwin Brady 15737d9Trickiness with implicits in dependent classesEdwin Brady 6f9ba3eAdded explicit error messages when eliminator/case function generation failsAhmad Salim Al-Sibahi d6ba4b2Added error reporting on eliminator generation failureAhmad Salim Al-Sibahi 17fe233Add scoped implicit argument to PiEdwin Brady 674eb4cSupport for inductive-inductive typesEdwin Brady fbcd643Check datatypes are not redefinedEdwin Brady c953ff0Add missing case in checkUniqueKind (fixed #1606)Mort Yao e90316aSupport type errors in docstringsDavid Raymond Christiansen 54dbb85Added TODOs and FIXMEs from the Elaborator for Data.Jan de Muijnck-Hughes 8698afcRemoved old comment from `src/Idris/Elab/Data.hs`Jan de Muijnck-Hughes 37292e1Save terms in docstringsDavid Raymond Christiansen 7e7368dStore kind in Pi bindersEdwin Brady bc2bcb6Add Borrowed typesEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady 41e9032Check constructor kinds for uniqueness errorsEdwin Brady a523c20Fix parameter identificationEdwin Brady ddced5cStore parameters in function typesEdwin Brady c72d0f4Split elaborator into multiple source filesEdwin Brady