git.iko.soy/Idris-dev
on aeb032a help sign in
history ofsrc/Idris/Prover.hs
all commits
f590608Reexport parseErrorDoc from Idris.ParserJason Felice 22587b2Make ParseError a newtypeJason Felice 5048ad4Introduce ParseError type aliasJason Felice e680962Return parse results using EitherJason Felice 1f8db23Import Trifecta qualified as PJason Felice 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice 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