git.iko.soy/Idris-dev
on 08ddbaa help sign in
history ofsrc/Idris/Core/TT.hs
all commits
783dddbFix Show for UNs.Matus Tejiscak 301752cRevert name mangling.Matus Tejiscak 589bb4bCtor erasure fixed.Matus Tejiscak f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen dd20facAdd semantic highlighting info for metavariablesDavid Raymond Christiansen 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 1a79f2bAdd a special name for instance constructors.Matus Tejiscak f0fe3ffAdd C codegen implementation of buffer primitivesShea Levy 149e816Add Buffer type and primitives to the coreShea Levy 41d3dafUse the pprint library to insert line breaksDavid Raymond Christiansen e46603aMerge remote-tracking branch 'upstream/master' into error-reflectionDavid Raymond Christiansen 8c620dcMerge remote-tracking branch 'upstream/master' into error-reflectionDavid Raymond Christiansen 9eb64f4Rewrite error printing to use the pretty-printerDavid Raymond Christiansen c0cc1ddMerge remote-tracking branch 'upstream/master' into semantic-pprintDavid Raymond Christiansen dc4ce0cReplace the string-slinging show with pretty-printDavid Raymond Christiansen fe3f03fAdded %error_reverse annotationEdwin Brady 5f0c449Colouring support in the proverDavid Raymond Christiansen 13f3c29Basic functioning with new pretty-printerDavid Raymond Christiansen 887b6e2Merge remote-tracking branch 'upstream/master' into error-reflectionDavid Raymond Christiansen e9c9297Make lookupCtxtExact return Maybe instead of ListDavid Raymond Christiansen 2c80895Bring my changes in line with the latest upstreamAlyssa Carter 06fd947Add "Can't solve goal" error messageEdwin Brady d711327Fix bug in 'forget' for well-typed termsEdwin Brady d82f5feMerge branch 'text-names'Edwin Brady 70ee9efMake more fields strictEdwin Brady 0c8c90dStrictness annotationsEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 66ec833Minor memory usage improvementsEdwin Brady fac49fcSome IBC compressionEdwin Brady bbee45cExplained the motivation of the name `P` for named referencesAlyssa Carter 770a3a7Display errors properly on IBC load failureEdwin Brady 8b7f8adPerformance improvement: name supplyEdwin Brady 4e6adebSeparate Core NFData instancesEdwin Brady cf58eebAdded some clarification of the purpose of `PVar`Alyssa Carter 2feffa9Added haddock comments for most of the rest of the functions in `Core.TT`Alyssa Carter 2ab9798Fixed typo: "unform" --> "uniform"Alyssa Carter 81e2e4aChanged my haddock comments to use proper markupAlyssa Carter ae37f9bAdding prefix to new record field namesAlyssa Carter 90eaa8dAdded haddock comments to a number of TT name manipulation functionsAlyssa Carter ab06192Adding haddock comments to `instantiate` and `substV`. Also clarified the third paramater of the `P` constructor for `TT`.Alyssa Carter 2162623Explained motivation for some cases in `termsize`Alyssa Carter