git.iko.soy/Idris-dev
on cb005bc help sign in
history ofsrc/Idris/Interactive.hs
all commits
17fe233Add scoped implicit argument to PiEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady 3ade599Partial evaluator fixesEdwin Brady 7e7368dStore kind in Pi bindersEdwin Brady 86b60b2Take .lidr syntax into account with :addmissingDavid Raymond Christiansen 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 c72d0f4Split elaborator into multiple source filesEdwin Brady 6cc18fdmakelemma fixEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 9907240Add new Err constructor to disambiguate the CantResolveAlts constructor.bmsherman f8759cdIDESlave support for setting the depth of interactive proof searchDavid Raymond Christiansen 094be98Add an optional depth to 'search' tacticEdwin Brady 659e985Add IDESlave support to :makelemmaDavid Raymond Christiansen a265279:makelemma now works on provisional definitionsEdwin Brady 719d472'search' now fails if there are metavariablesEdwin Brady 50f63b5Make sensible implicit choices in :addlemmaEdwin Brady f8e6549:addclause now adds template bodies to instancesEdwin Brady db88c3eTidy output of :makelemmaEdwin Brady af99a9dAdd :makelemma command in interactive editingEdwin Brady dae7d7dMove interactive commands to their own moduleEdwin Brady