git.iko.soy/Idris-dev
on 7afa310 help sign in
history ofsrc/Idris/Core/ProofState.hs
all commits
3ade599Partial evaluator fixesEdwin Brady 971d88dAnnotate several top-level functionsMichael Maloney 7e7368dStore kind in Pi bindersEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady ab36099Use a zipper-like proof stateEdwin Brady a9dd2e4Lift out proof term into a separate moduleEdwin Brady e6e1ad9Unification fixEdwin Brady 0a1965eChange 'Not a guess' errorEdwin Brady 8ed343bRemove dodgy unification hackEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 4833cb3Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetacticAhmad Salim Al-Sibahi 5045daeAdded tactic for case analysis. Also, induction now work on expressions instead of simply names.Ahmad Salim Al-Sibahi a0b05e2Allow induction on terms instead of simply namesAhmad Salim Al-Sibahi 921b766Fix name propagation in error messagesEdwin Brady 41f921fUnify more things!Edwin Brady d10c1e9Can't assume explicit names in updateSolvedEdwin Brady 5a5eecaMerge pull request #1143 from ahmadsalim/bug/inductionfixDavid Christiansen e36c883Fix #1015raichoo 78ff448Bug fixing of induction bugsAhmad Salim Al-Sibahi 62705e4Tweak mergeNotunifiedEdwin Brady f2bf55dMerge 'not unified' variablesEdwin Brady 51394aaAdd 'unify' tacticEdwin Brady ff742feActually track applications in the elaborator wrt unification failsDavid Raymond Christiansen b38bc03Add basic elaboration context tracking to unificationDavid Raymond Christiansen d88d1caFixes idris-lang/Idris-dev#971. Renames induction holes such that they are unique in context.Ahmad Salim Al-Sibahi 88f88ebUnification tweak; better disambiguationEdwin Brady 1f897b1Fix for matchProblemsEdwin Brady ecfb293Evaluator bug fixEdwin Brady 6d3863dBetter environment management in unificationEdwin Brady 2cff556Another unification fixEdwin Brady c959fb0Unification changesEdwin Brady 41d3dafUse the pprint library to insert line breaksDavid Raymond Christiansen 13f3c29Basic functioning with new pretty-printerDavid Raymond Christiansen 1dfc8fdFix typo that led to unification bugEdwin Brady d82f5feMerge branch 'text-names'Edwin Brady 0c8c90dStrictness annotationsEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady a611debFix memory leakEdwin Brady dfc3e44Shave a bit more off IBC sizeEdwin Brady ba15257Another small reduction in calls to TT.(==)Edwin Brady f47329cShortcut unification updatesEdwin Brady 4e6adebSeparate Core NFData instancesEdwin Brady fa364caCheck for cyclic solutions in unificationEdwin Brady fef1207Make note of unapplied unifiation solutionsEdwin Brady 3191f16Induction works for all types with eliminators now (some eliminators still need fixing) including those with indicies.Ahmad Salim Al-Sibahi d7f4e11Induction now works on types with parametersAhmad Salim Al-Sibahi 0700c58Fix another INTERNAL ERROREdwin Brady 2f5c756Better error message for 'Not a guess'Edwin Brady 67da31aMerge branch 'master' into cabal-libraryBrian McKenna 5000aebAdd a Cabal libraryBrian McKenna