Epilogue

First instalment of an Epigram 1 change I’ve been intending to do for ages. Almost no effort required! I’ve fixed things so that variables named but not declared in the premises of a rule get inserted implicitly at the left end of the rule (as James McKinna used to argue) rather than as locally as possible (as Randy Pollack used to argue). vcons now gets X and n implicitly before x and xs; n used to come in the middle, unless you explicitly forced it leftward. Generally, I find that partial applications work more pleasantly more often with James’s convention. You can still force things rightward with an explicit premise (which doesn’t mean the arg has to be explicit).

Anyhow, I imagine this change may cause minor damage. I’ve tried a few examples, and I had to tweak a thing or two: mostly stuff that was a bit chancy anyway and should have been cleaned up long ago. I suggest that regulars try out their favourites and howl if they aren’t readily fixable.

There will be a second and more subtle change: at the moment, uninstantiated metavariables in rules are generalised to yield implicit arguments wherever they end up; these also should be shunted leftward where possible. Probably won’t do any damage, except to code which relies on the current morally random placement.

I don’t think we should generate new binaries just yet; I’ll try and get this cleaned up as soon as possible.

This entry was posted on Friday, October 21st, 2005 at 10:21 am and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.