git.iko.soy/Idris-dev
on d7b2913 help sign in
history ofCHANGELOG
all commits
770a3a7Display errors properly on IBC load failureEdwin Brady c486513Added label type 'nameEdwin Brady fef1207Make note of unapplied unifiation solutionsEdwin Brady 6749dd5Mention preorder reasoning in CHANGELOGDavid Christiansen a10bcf0Tweak CHANGELOGv0.9.10Edwin Brady 3000418Update CHANGELOGEdwin Brady c459480Improve type class overlap checkEdwin Brady d762b28Update CHANGELOGEdwin Brady fcc4c0aAdded note about changes to [..] in the CHANGELOGDavid Christiansen afef29eUpdate CHANGELOG and verison numberEdwin Brady 0f926d7Update CHANGELOGEdwin Brady 66cc7f9Bring CHANGELOG up to dateEdwin Brady d2f5480Update CHANGELOGEdwin Brady 6d9f01cUpdate CHANGELOGEdwin Brady 0e76ac9Remember whether implicits are machine generatedEdwin Brady 822b518Merge pull request #479 from david-christiansen/repl-persistent-historyEdwin Brady c93a2d4Merge pull request #478 from david-christiansen/repl-initEdwin Brady 8000794Final (I hope!) implementation paper tinkeringEdwin Brady 36d05d1CHANGELOG update for REPL historyDavid Christiansen c778c24Update CHANGELOG for init scriptsDavid Christiansen 2a0885eBetter representation and rendering of generated namesEdwin Brady bd70f22Update CHANGELOG for colours in REPLDavid Christiansen 6dc5ea2Fix name shadowing in whereEdwin Brady 48d1105Added 'quoteGoal x by p in e' syntax meaning, let x = p [current goal] in e Additionally, the value of x is normalised, which means p can be a compile-time only %reflection function used to prove something interesting in e. See test030 for an example of automated proof by reflection.Edwin Brady fd9bd68Add '%reflection' option for functions A reflection function can evaluate at compile-time only, and pattern matches on *syntax* rather than on constructor forms. Also add 'prim__syntactic_eq' for a compile-time syntactic equality check.Edwin Brady 506d367"it" now refers to the previous value at the REPLEdwin Brady 55dbed5Update CONTRIBUTORS and CHANGELOGEdwin Brady f27d3bbUpdate CHANGELOGEdwin Brady 1cfda6cUpdate CHANGELOGEdwin Brady 61d39daSwapped Vect arguments So now nicer to write type class instances for Functor, Applicative, etcEdwin Brady 2e8904dMuch faster coverage checking by ignorng forced arguments No need to generate cases to check for them, because we already know their value is forced by another part of the same constructor!Edwin Brady b543b29Allow names to be attached to provisional definitions lhs ?= {name} rhs -- generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional - a unique name is generated if it is absent.Edwin Brady 7af449cUpdate CHANGELOG to reflect recent additions and fixesEdwin Brady 5b2f091Allow type class constraints in 'using' clauses e.g. if a using block is given asEdwin Brady 442d8c8Fix parameter identification in data declarations Fixes issue #259Edwin Brady 43d915dMerge branch 'master' of github.com:edwinb/Idris-devEdwin Brady f1e61daIf the goal is not a function type when elaborating \, invent one ...and attempt to solve it by unificationEdwin Brady d8cff54Dynamic libraries and REPL IO in CHANGELOGDavid Christiansen 35034dbChange forall tactic to use unify rather than isType Fixes issue #189Edwin Brady 1a87674Improved type-directed name disambiguationEdwin Brady 5593697Rename EFF to EFFECT (for more consistent naming rules)Edwin Brady abb2c24Remove Threading effect (on account of it not working :))Edwin Brady 022d4dfAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!Edwin Brady 2396796Merge branch 'javascript' of https://github.com/raichoo/Idris-dev into raichoo-javascriptEdwin Brady 12189d7Normalise type before checking it's a valid postulateEdwin Brady 06bfa75Fix error in conversion check Fixes issue #187Edwin Brady c020e50javascript: split javascript and node targetraichoo 2a13be4Distinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon!Edwin Brady a6ed7c3javascript: got rid of --javascript use --targetraichoo 17e40d2Update CHANGELOGEdwin Brady