git.iko.soy/Idris-dev
on fd6898e help sign in
history ofsrc/Idris/ProofSearch.hs
all commits
fdfd99eFix behaviour of %hideEdwin Brady 0c5b397Revert to old behaviour on expression searchEdwin Brady 1cf8fe9Context for "Can't find implementation"Edwin Brady 74926ffRenamed Prelude.Classes to Prelude.InterfacesJan de Muijnck-Hughes acbcadbUnrelated misc golf.Leif Warner c7bed76Better disambiguation with type class methodsEdwin Brady 83f0af1Display expected type of RHS in error messagesEdwin Brady 83ca4aeFriendlier error on proof search failureDavid Raymond Christiansen c931effProof search improvementsEdwin Brady 47db070Proof search fixEdwin Brady d3b66cdSlight relaxation of proof search rulesEdwin Brady 55ffc21Some display tweaks for explicit argumentsEdwin Brady f5aecf7Deferred autosEdwin Brady 81e1962Type class resolution shouldn't use match_applyEdwin Brady 239c8caMove resolveTC to ProofSearch.hsEdwin Brady 6e7c036Allow single constructor types in proof searchEdwin Brady 57ba18dSlightly relax check for proofsearchabilityEdwin Brady 5a08c2cProof search tweakEdwin Brady 7095d6cProof search should only use user visible namesEdwin Brady 8dd2a7fMake interactive proof search less enthusiasticEdwin Brady 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen 0d01d0dMore precision for trivialEdwin Brady 3034fb6Remove argument ordering hack in elaboratorEdwin Brady 8984d49Remove PRefl and all references to itMelvar Chen f987aecAdd info field to AppEdwin Brady 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