git.iko.soy/Idris-dev
on a37fc8a help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
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 cebd1b4Merge pull request #1315 from david-christiansen/serialized-termsDavid Christiansen e245d48Maintain pretty-printer bound varsDavid Raymond Christiansen 80d1a88Fix implicit spotting in case blocksEdwin Brady d1a832aSend serialized versions of TT terms in pprintDavid Raymond Christiansen 4833cb3Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetacticAhmad Salim Al-Sibahi 9993f3bAdd pi to overridable syntax in DSL blocksDavid Raymond Christiansen 5045daeAdded tactic for case analysis. Also, induction now work on expressions instead of simply names.Ahmad Salim Al-Sibahi a0b05e2Allow induction on terms instead of simply namesAhmad Salim Al-Sibahi baaea97Merge pull request #1288 from david-christiansen/issue/1286David Christiansen d6c5b2bAdd semantic highlighting for postulatesDavid Raymond Christiansen