git.iko.soy/Idris-dev
on 1b71663 help sign in
history ofsrc/Idris/Core/Elaborate.hs
all commits
cc7ef9aRemove old eliminator generation and induction tactic (#4351)Ahmad Salim Al-Sibahi 3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice 4ade674Fix disambiguation on LHSEdwin Brady b7cf1ecFix delab of scoped implicitsEdwin Brady a1e3b5bRevert to normalising from WHNFEdwin Brady 2f3c9a5Add RigCount to pattern bindingsEdwin Brady 491633bSyntax for linear argumentsEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady 2196023Fix patvar naming for implicitsEdwin Brady d0671a3Use WHNF in a few placesEdwin Brady b0130d6Add whnfArgsEdwin Brady 7537cc4Change totality checking and inliningEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) dd6c823Avoid unnecessary normalisation in mkClaimsEdwin Brady 7e0c70aFix potential loop in prepare_applyEdwin Brady 08cef17HLint DIrected Code CleanupJan de Muijnck-Hughes fdfa04cStore file with constraints + exportEdwin Brady 83ef000Check delayed holes are still holesEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes cba27c8Normalise type when introducing lambdaEdwin Brady 92a4d84Implicit bindings warningsEdwin Brady eaf5211Add the ability to define datatypes in ElabDavid Raymond Christiansen 6eaf933Disambiguation tweakEdwin Brady 3d2fa6cBetter elaboration of applicationsEdwin Brady 83f0af1Display expected type of RHS in error messagesEdwin Brady 18e4b21Minor change to display of metavariablesEdwin Brady 93dafdeMake sure deferred names are uniqueEdwin Brady c931effProof search improvementsEdwin Brady b693b81Merge pull request #2540 from david-christiansen/wip/tacticalDavid Christiansen ab63941Added top-level %runElab supportDavid Raymond Christiansen 0140e67Tweak to hole liftingEdwin Brady 7095d6cProof search should only use user visible namesEdwin Brady 212587bRemove 'score' and guesswork from error messagesEdwin Brady e1c79efBetter error when no alternative is validEdwin Brady 5da0d60Faster processing of alternativesEdwin Brady 0dd2f06Restrict (and speed up) implicit coercionsEdwin Brady ff60396Make apply match internal behaviourDavid Raymond Christiansen 4ede52dAllow the pretty-printing of Raw termsDavid Raymond Christiansen c66bf01Don't uniquify MN patvar names in reflected ElabDavid Raymond Christiansen 2c609aeEnvironment fix in prepare_applyEdwin Brady 0819777Improved type-directed disambiguationEdwin Brady 3034fb6Remove argument ordering hack in elaboratorEdwin Brady 8073344Better errors on stuck reflected elaboratorsDavid Raymond Christiansen d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen f987aecAdd info field to AppEdwin Brady