git.iko.soy/Idris-dev
on bf4e535 help sign in
history ofsrc/Idris/ProofSearch.hs
all commits
927fc19Prune proof searchEdwin Brady a0725d2Fix trivial top level proof search failureEdwin Brady 13a36a3Annotate functions as %hint for auto searchEdwin Brady ec06f94Change to a recoverable error in proof searchEdwin Brady 39e4eb0IO primitives tweak to support JSEdwin Brady 6faa820Do more reduction in proof searchEdwin Brady 48715b7Compute before proof searchEdwin Brady b0a0c0cImprovement for 'auto'Edwin Brady 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