git.iko.soy/Idris-dev
on 385dcbf help sign in
history ofsrc/Idris/ProofSearch.hs
all commits
e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady f467346Detect implicit parameters to interfacesEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) 53fae80use interface in error message when check instancezjhmale c3f0755replace code level class symbol with inferfacezjhmale 08cef17HLint DIrected Code CleanupJan de Muijnck-Hughes 22792d2Use ParentN for its intended purposeMelvar Chen 0896073Added documentation for modules.Jan de Muijnck-Hughes 1019ce5Source file stylings & Haddock.Jan de Muijnck-Hughes 37aa54aSearch open instances firstEdwin Brady 254a227More control over resolving named implementationsEdwin Brady 1726bf9Changed type classes in error messages and documentation to interfaces where necessary (previously forgotten)Ahmad Salim Al-Sibahi 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