git.iko.soy/Idris-dev
on be22ac6 help sign in
history ofsrc/Idris/Prover.hs
all commits
f4aaf01Guard !! in forgetEnvEdwin Brady 426d052Add provenance flag to unification errorsEdwin Brady 83793a6Add the ability for IDEs to get documentation overviewsDavid Raymond Christiansen c5de844Catch some lingering renames that I missedDavid Raymond Christiansen b85b2ebRename ideslave to ide-modeDavid Raymond Christiansen d5377beNew language-dependent FFIEdwin Brady 26da5c7Save index file when installing a packageEdwin Brady 5faaba9More information runtime error for missing caseEdwin Brady 0d8a153New way of dealing with unmatchable patternsEdwin Brady ba51147Removing matching on PSEdwin Brady 6b6aae0Avoid retrying unification problems constantlyEdwin Brady b0a0c0cImprovement for 'auto'Edwin Brady f1e161dA new primitive tactic for getting source locationsDavid Raymond Christiansen 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