git.iko.soy/Idris-dev
on db07875 help sign in
db07875Merge "add definition" and "add missing" commandsEdwin Brady 8996abfParse to line now reads whole definitionEdwin Brady c98e24fMerge pull request #2746 from david-christiansen/pruvilojDavid Christiansen f7e1990Add lookup of FunArgs for global names to ElabDavid Raymond Christiansen 6a208f7Fix docstrings for apply and matchApplyDavid Raymond Christiansen c5f5dabMerge pull request #2741 from david-christiansen/pruvilojDavid Christiansen 5323b12Remove obsolete Elab primitive from Term.hsDavid Raymond Christiansen 5330e8aSimplifications to ElabDavid Raymond Christiansen ab62c98Make cycle test work with Curses IdrisDavid Raymond Christiansen 1edba41Add environment argument to Elab.Tactics.checkDavid Raymond Christiansen 68c519eConvert comments in WHNF.hs to HaddockDavid Raymond Christiansen d2f892bMerge pull request #2728 from jeremy-w/jeremy-w/ipkg-allow-arbitrary-executable-names-2721Niklas Larsson aabda6eMerge pull request #2735 from LeifW/bump_vector_constraintNiklas Larsson 304a7e7Bump vector constraint to allow 0.11.xLeif Warner 8bd99edDetect cycles in importsEdwin Brady fe38aacCache information when module chasingEdwin Brady 4249691Check whether type declarations are actually typesEdwin Brady 9229b62PParser.hs: filename: Add check that path is validJeremy W. Sherman ee589b5PParser.hs: Use ConstraintKinds to avoid "illegal tuple constraint"Jeremy W. Sherman b329791Add @jeremy-w to CONTRIBUTORSJeremy W. Sherman 6c4deb2Merge pull request #2718 from david-christiansen/pruvilojDavid Christiansen 16ed52dMerge pull request #2719 from jeremy-w/jeremy-w/edit-elaborator-reflectionNiklas Larsson 9c8d8ccCHANGELOG: Fix typo: mutliple -> multipleJeremy W. Sherman 4f96945Test that IPKG rejects executable with directory componentJeremy W. Sherman a22dd61Add test that quoted strings with valid filenames are OKJeremy W. Sherman 4274456Add test that IPKG executable accepts namespaced identifierJeremy W. Sherman 67ff67ePParser.hs: filename: Explain failed parse with |fail|Jeremy W. Sherman 3ccdc4bPParser.hs: filename: Verify it is a non-empty filenameJeremy W. Sherman 44b87ecPParser.hs: filename: Restore backwards compatibilityJeremy W. Sherman 5eeaf9ePParser.hs: filename: Remove use of |try|Jeremy W. Sherman d75e4c6Remove advice to import Language.Reflection.ElabJeremy W. Sherman c6c4bf4Drop claim that general-purpose commands are general REPL commandsJeremy W. Sherman d17f246Remove duplicated phraseJeremy W. Sherman f30db6bFix typo: reply -> REPLJeremy W. Sherman 1e687f3Rename record fields in reflectionDavid Raymond Christiansen ffa41abCONTRIBUTING.md: Fix typo "Factroy" -> "Factory"Jeremy W. Sherman b6a8a95PParser.hs: Parse executable clause argument as filenameJeremy W. Sherman c772bf5PParser.hs: Add |filename| parserJeremy W. Sherman 6a7b071Update the list of elaboration shell commandsJeremy W. Sherman be11838Removes :q alias for :abandonJeremy W. Sherman c18bf77Rephrases section "Interactively building elaboration scripts"Jeremy W. Sherman 83ca4aeFriendlier error on proof search failureDavid Raymond Christiansen 4f68012Convert some datatypes to records in reflectionDavid Raymond Christiansen 6ca7c4fAdd reflexivity tactic to PruvilojDavid Raymond Christiansen 002e9b9elaborator-reflection.rst: Fix rendering of bulleted listJeremy W. Sherman 2cda43eUpdate docs testEdwin Brady 3268c1bChange documentation of mapEdwin Brady c7efd0aMerge pull request #2714 from david-christiansen/no-more-ugly-scriptDavid Christiansen 0f89577Remove NErasedDavid Raymond Christiansen be03634Merge pull request #2712 from david-christiansen/no-more-ugly-scriptDavid Christiansen