git.iko.soy/Idris-dev
on ccda94e help sign in
history ofsrc/Idris/Interactive.hs
all commits
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