git.iko.soy/Idris-dev
on c629b60 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
ba0b525Pretty-printing of implicit args to (=)David Raymond Christiansen 7ce4d90Add annotations for :search result classificationbmsherman 893b980Add :printdef command to show the definition of a pattern-matching operationDavid Raymond Christiansen ce7dff9Error when using empty namespace for disambiguation at REPLDavid Raymond Christiansen 7e7368dStore kind in Pi bindersEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady ddced5cStore parameters in function typesEdwin Brady 93f407dUse strings for code generatorsEdwin Brady 3d1a728Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 788f800Record import paths in ibcEdwin Brady ecea9adMerge branch 'master' into repl-definitionsAlyssa Carter d947282Merge pull request #1452 from hannesm/ideslave-socketDavid Christiansen 480024cRemove all the handle argumentsDavid Raymond Christiansen 2418336Save some allocations in updateSolvedEdwin Brady ab36099Use a zipper-like proof stateEdwin Brady 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 be0a480provide a new option, --ideslave-socket, for an ideslave listening on a socketHannes Mehnert ef36111Merge branch 'master' into repl-definitionsAlyssa Carter 382542aAdd %no_implicit directiveEdwin Brady c72d0f4Split elaborator into multiple source filesEdwin Brady 84b172aAdd tactics "skip" and "fail"David Raymond Christiansen ae9b938Merge branch 'master' into repl-definitionsAlyssa Carter f38b611Make Idris build with the latest hackageDavid Raymond Christiansen 5c4f5d2Added an :unlet/:undefine command.Alyssa Carter 2aed52aUpdate docs for equality typeDavid Raymond Christiansen c1968edFix parameter spotting in function typesEdwin Brady 7d95becMake type search work in the proverDavid Raymond Christiansen 6340534Merge pull request #1371 from david-christiansen/prover-output-colorDavid Christiansen c29e746Allow :doc in proverDavid Raymond Christiansen 1269791Keep type arguments of = when unelaboratingEdwin Brady 9af885aHighlight differing implicits in errorsEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 3c4bd14Merge pull request #1361 from trillioneyes/repl-definitionsEdwin Brady 98352eeComment clarification.Matus Tejiscak c1277c8Handling more forms of definition.Alyssa Carter c201192Bring erasure info to the case tree builder.Matus Tejiscak d8ed044Add getInaccessibleArgs.Matus Tejiscak a5e8ca3Changed :let to work with an arbitrary number of `PDecl`s (though only one name at a time for now).Alyssa Carter e260741Preliminary support for a :let command in the replAlyssa Carter dac312bAdd goal types to quasiquotes.David Raymond Christiansen e08a18dMerge remote-tracking branch 'refs/remotes/upstream/master' into quasiquoteDavid Raymond Christiansen c90d4b4Parsing for quasiquotesDavid Raymond Christiansen 67f7373Support builds that doesn't use cabal for libs and rtsniklas 48a9659fix spelling of "parenthesise"Ricky Elrod 22b2548Merge pull request #1323 from bmsherman/parenthasizeInfixDavid Christiansen c4eca4fMerge branch 'master' into parenthasizeInfixbmsherman 7d38943Proper and complete parenthasization of infix operator names.bmsherman fc6f5feMerge pull request #1322 from bmsherman/equalDeclDavid Christiansen c4ce749Parenthasize infix names in REPL outputbmsherman 802c248Make type arguments in (=) declaration implicit (for docs)bmsherman