git.iko.soy/Idris-dev
on 7afa310 help sign in
history ofsrc/Idris/ProofSearch.hs
all commits
9ceece1EXPERIMENTAL uniqueness typesEdwin Brady 094be98Add an optional depth to 'search' tacticEdwin Brady a6d79abFix silly error in 'search'Edwin Brady 719d472'search' now fails if there are metavariablesEdwin Brady e07c13dAdd :refine (:ref) command for refining a holeEdwin Brady c1ef938New syntax for documentation commentsDavid Raymond Christiansen b651aafProof search fixEdwin Brady 85e68a7Improve inference in monadic codeEdwin Brady 3848c07Record partial type inference infoEdwin Brady 0ab30e7Restrict error reflection scope to one argumentDavid Raymond Christiansen 5000aebAdd a Cabal libraryBrian McKenna 3c32b65Whitespace cleanup.George Leontiev b7b55b7Allow hints to be given to proof searchEdwin Brady b16baadLeave metavariables for unfinished proofsEdwin Brady 53ce3ccProof search now also tries recursive callsEdwin Brady dcdbcc3Proof search now tries appropriate constructorsEdwin Brady 5d2d5a7Failed proofsearch branch creates new metavariableEdwin Brady abf99a5Add proofsearch tactic, with :ps at the REPLEdwin Brady