git.iko.soy/Idris-dev
on 385dcbf help sign in
history ofsrc/Idris/Prover.hs
all commits
aa0b315Merge pull request #3847 from be5invis/be5invis-do-rewriteNiklas Larsson 4a1c2a1Refactoring: Move options out of AbsSyntaxNiklas Larsson 96a982aAdd do-rewritebe5invis e3daf28Add RigCount to environmentEdwin Brady 521b8bfRemove unused case tree codeEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan a09a1bfBuild with GHC8 and trifecta-1.6David Kraeutmann fdfa04cStore file with constraints + exportEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes eaf5211Add the ability to define datatypes in ElabDavid Raymond Christiansen 76c46bbMore flexible holesEdwin Brady 2aae0b3Do not quit the REPL on Ctrl-C.Alexander Shabalin 1b3bffaProver.hs: foldl (++) [] . map -> concatMapHeather f4c91c6In interactive elaborator, show all premisesDavid Raymond Christiansen 81a9095Add deprecation warning to old interactive proverDavid Raymond Christiansen 8902cacSave context changes in interactive elabDavid Raymond Christiansen 6432db2Show MNs that occur in the goal in the interactive proversDavid Raymond Christiansen 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen a3407cbDisplay 'Hole' instead of 'Metavariable'Edwin Brady 202c913Logging levels must be explicitly mentioned.Jan de Muijnck-Hughes d2beadc7.10 compatibilityDavid Raymond Christiansen fbbe433Rename function to better reflect purposeDavid Raymond Christiansen 54cd5a6An interactive Elab shellDavid Raymond Christiansen 4dabdbaPropagate errors originating from case treesDavid Raymond Christiansen c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen c380421Move ElabTerm into Elab.TermEdwin Brady 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