git.iko.soy/Idris-dev
on 7afa310 help sign in
history ofsrc/Idris/Core/TT.hs
all commits
7ce4d90Add annotations for :search result classificationbmsherman 971d88dAnnotate several top-level functionsMichael Maloney 486c4c0Add missing pattern in TT.hsMichael Weiss 7e7368dStore kind in Pi bindersEdwin Brady bc2bcb6Add Borrowed typesEdwin Brady e30ff97Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady a1fb7a3Inline with blocksEdwin Brady 2aaff41Stop erasing binder types in executorDavid Raymond Christiansen 9abbc3fCache uniqueness information in NameTypeEdwin Brady 41e9032Check constructor kinds for uniqueness errorsEdwin Brady 7cc7c32Make top level type 'Type*'Edwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady 788f800Record import paths in ibcEdwin Brady 42c694cMore efficiency improvementsEdwin Brady 84b172aAdd tactics "skip" and "fail"David Raymond Christiansen c1968edFix parameter spotting in function typesEdwin Brady 5ffef89Type class resolution fixEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady e245d48Maintain pretty-printer bound varsDavid Raymond Christiansen d1a832aSend serialized versions of TT terms in pprintDavid Raymond Christiansen d6c5b2bAdd semantic highlighting for postulatesDavid Raymond Christiansen 21124c3Merge remote-tracking branch 'upstream/master' into cantResolveAltsbmsherman 282abc8Enable pretty printing of CantResolveAlts errors.bmsherman 9907240Add new Err constructor to disambiguate the CantResolveAlts constructor.bmsherman 6d6e48bMerge pull request #1258 from bmsherman/uniqueBindersEdwin Brady a2028e1Modified uniqueBinders function to prevent overlapping binders.bmsherman e7a35e9Remove implicit qualifier for 'effect'Edwin Brady e16c068Documentation for primitivesDavid Raymond Christiansen 89a975eImprove ideslave highlighting of primitivesDavid Raymond Christiansen 8081528Make Ctxt lookups more straightforward in ASTUtils.Matus Tejiscak 78ff448Bug fixing of induction bugsAhmad Salim Al-Sibahi cfbb64fMerge branch 'idrisdoc' of github.com:PhilipRasmussen/Idris-dev into PhilipRasmussen-idrisdocDavid Raymond Christiansen bb6873cAdd ASTUtils.Matus Tejiscak 783dddbFix Show for UNs.Matus Tejiscak 301752cRevert name mangling.Matus Tejiscak 589bb4bCtor erasure fixed.Matus Tejiscak 20e0bf4Merged with masterPhilip Rasmussen f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen dd20facAdd semantic highlighting info for metavariablesDavid Raymond Christiansen e21b167Tiny tidying upPhilip Rasmussen 57c3ffcAdd application context to all error messagesDavid Raymond Christiansen f01873fAdd stack of elaboration context to ElaboratingArgDavid Raymond Christiansen fb3f7f0Use At to hold FCsDavid Raymond Christiansen aed179cTrack the providence of unification errorsDavid Raymond Christiansen ff742feActually track applications in the elaborator wrt unification failsDavid Raymond Christiansen e9ef380Support text formatting in docstringsDavid Raymond Christiansen 15aebc9Add highlighting for keywords in interpreter outputDavid Raymond Christiansen 7437ebePrepared data structure of FC for spanning, and added the span of the last token parsed to IdrisAhmad Salim Al-Sibahi cb4b145Merge pull request #942 from ziman/instance-ctorsEdwin Brady d4ffc21Add ManagedPtr typeEdwin Brady