git.iko.soy/Idris-dev
on 7afa310 help sign in
history ofsrc/Idris/Prover.hs
all commits
497caf0Make output from :t name annotate with termsDavid Raymond Christiansen 705dbe1Stop encoding prover messages as outputDavid Raymond Christiansen 02e8f8cSend prover errors back with spans instead of ANSIDavid Raymond Christiansen 4fe16a5read from handle rather than stdinHannes Mehnert 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 8f7d848Don't show irrelevant MNs in proverDavid Raymond Christiansen c72d0f4Split elaborator into multiple source filesEdwin Brady 29c02f4Fix scope/matching issues in proof scriptsEdwin Brady 7d95becMake type search work in the proverDavid Raymond Christiansen c29e746Allow :doc in proverDavid Raymond Christiansen 3a2c8aaMake prover better at IDESlave protocolDavid Raymond Christiansen e363c09Better treatment of unbound implicitsEdwin Brady c201192Bring erasure info to the case tree builder.Matus Tejiscak c4eca4fMerge branch 'master' into parenthasizeInfixbmsherman 7d38943Proper and complete parenthasization of infix operator names.bmsherman e245d48Maintain pretty-printer bound varsDavid Raymond Christiansen d1a832aSend serialized versions of TT terms in pprintDavid Raymond Christiansen 7623850IDESlave protocol fixes in case of errorDavid Raymond Christiansen 2494a8aReorder code to make it more readableDavid Raymond Christiansen 387b738Remove unnecessary partialityDavid Raymond Christiansen 6d0abfbCorrect IDESlave protocol violations in proverDavid Raymond Christiansen 2d22462Check that proof steps introduce no new problemsEdwin Brady 8e55b64Show let bindings with proper line breaks and indentation in proverDavid Raymond Christiansen 9491c3cAdd ppOptionIst function.Peter Minten 5e3c248Change impl argument to a pretty printing opt recordPeter Minten bfe6499Give the pretty-printer access to info about infixesDavid Raymond Christiansen 62705e4Tweak mergeNotunifiedEdwin Brady 140d8d2Add check after each proof step, not just the endEdwin Brady b1d2553Respect accessibility in case tree elaboration.Matus Tejiscak f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen 7faf4e8Show argument names in :docDavid Raymond Christiansen b38bc03Add basic elaboration context tracking to unificationDavid Raymond Christiansen 423b4c4Allow users to disable the auto-solve in the proverDavid Raymond Christiansen bd744f1Propagate function name to tacticsEdwin Brady af0171eProver commands for evaluation and typechecking expressionsDavid Raymond Christiansen d95808eDon't give INTERNAL ERROR when abandoning a proofEdwin Brady da24632Render using console widthDavid Raymond Christiansen 94c4cf8Make prover respect showimplicits from IStateDavid Raymond Christiansen 5f0c449Colouring support in the proverDavid Raymond Christiansen 13f3c29Basic functioning with new pretty-printerDavid Raymond Christiansen d82f5feMerge branch 'text-names'Edwin Brady 0c8c90dStrictness annotationsEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 7604451Cache argument types for building case treesEdwin Brady 5000aebAdd a Cabal libraryBrian McKenna f18d79cRemove calls to "error". Fixes #607.David Christiansen 6b16b47Fix display of errors in proverDavid Christiansen 3c32b65Whitespace cleanup.George Leontiev f34f0afBetter display of metavariable types in :tEdwin Brady