1afc64051b44cc6b3e1918d8d27f1b9ced788f3a Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/4f4309262d414229ebb6dc1ee9d58fb0f4afbfaa 4f4309262d414229ebb6dc1ee9d58fb0f4afbfaa

2009-07-05T23:11:27-07:00

Refactored subst function. 74847900bc1637a12a63aaba93b4dd844fdb684d Luke Palmer lrpalmer@gmail.com 64244cd14368ac553846d9e33ff15f1cf3f151da Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/1afc64051b44cc6b3e1918d8d27f1b9ced788f3a 1afc64051b44cc6b3e1918d8d27f1b9ced788f3a

2009-07-05T21:03:40-07:00

A little user-interface cleanup. d08bd02e520170e342a8dfb6b66e3e95fce7cc6a Luke Palmer lrpalmer@gmail.com bc543bcbd430e6597125827b8f8f771a715aff82 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/64244cd14368ac553846d9e33ff15f1cf3f151da 64244cd14368ac553846d9e33ff15f1cf3f151da

2009-07-05T20:58:19-07:00

Did I fix DepthLazyNF? a60ead6678c7fa7d9154eae118178733dbca2c77 Luke Palmer lrpalmer@gmail.com 778107ae13886b765d01eb3d23292cc48bfd9177 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/bc543bcbd430e6597125827b8f8f771a715aff82 bc543bcbd430e6597125827b8f8f771a715aff82

2009-07-03T14:16:28-07:00

Added a *broken* DepthLazyNF. dc8c25cd889cb831f6c1e423069579c31f3dde15 Luke Palmer lrpalmer@gmail.com 501e8771fc13b4f52a024f6ca8fa1f1946317da0 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/778107ae13886b765d01eb3d23292cc48bfd9177 778107ae13886b765d01eb3d23292cc48bfd9177

2009-07-03T13:54:58-07:00

Manually playing with symbols for understanding. ca271fcb46edc294e869e6a1d422a9476c938d8b Luke Palmer lrpalmer@gmail.com 7f44febbc2dda2a7a997fcea361cc5069a72828c Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/501e8771fc13b4f52a024f6ca8fa1f1946317da0 501e8771fc13b4f52a024f6ca8fa1f1946317da0

2009-06-30T17:07:50-07:00

Identified an area that breaks sharing in LazyNF. 161a09393cccdefbfa5a541592cac70e7a03ef84 Luke Palmer lrpalmer@gmail.com 78ee9b0b89eed379760e88046c8c4e49fb2f5e36 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/7f44febbc2dda2a7a997fcea361cc5069a72828c 7f44febbc2dda2a7a997fcea361cc5069a72828c

2009-06-30T13:39:35-07:00

Teensy little bit of cleanup. 0dfb453c8db1130d7fe709de983e90c555c246fd Luke Palmer lrpalmer@gmail.com 86f87151bcce9fb81bb201d06f5d49c48b0cdd69 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/78ee9b0b89eed379760e88046c8c4e49fb2f5e36 78ee9b0b89eed379760e88046c8c4e49fb2f5e36

2009-06-29T15:13:07-07:00

Added a note about YNF reduction, a potential infinite unfolding solution. b3952e3450668a5391ed7f2b9dc4accb27cc9f5e Luke Palmer lrpalmer@gmail.com e61dfc5f29468b017963806808554e493273bb49 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/86f87151bcce9fb81bb201d06f5d49c48b0cdd69 86f87151bcce9fb81bb201d06f5d49c48b0cdd69

2009-06-19T02:46:52-07:00

Brought the cabal file up to date. Still a clean build with no extensions :-) 89ec8771225f67bba09e1b0fb34a16a49c23cb2b Luke Palmer lrpalmer@gmail.com ab06f38962ab3a3a861db0185d021db088b0b43b Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/e61dfc5f29468b017963806808554e493273bb49 e61dfc5f29468b017963806808554e493273bb49

2009-06-19T02:34:58-07:00

Removed the XIH rule. b9a94653f29915c802a97cf5ebe5606b098a07c5 Luke Palmer lrpalmer@gmail.com 558100d9cc96aab0ea59f0ea4a9a4850847c75d8 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/ab06f38962ab3a3a861db0185d021db088b0b43b ab06f38962ab3a3a861db0185d021db088b0b43b

2009-06-19T02:28:03-07:00

Proved the application theorem on function types. In desperate need of more automation, the plumbing is getting out of hand. 78ea6f00df7ef749b1304551784ea6dd1ea878d2 Luke Palmer lrpalmer@gmail.com 31d84832cd129ac1b06c75c73169a38d8a259d35 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/558100d9cc96aab0ea59f0ea4a9a4850847c75d8 558100d9cc96aab0ea59f0ea4a9a4850847c75d8

2009-06-19T01:17:26-07:00

Yet more rigorous symbol definitions. Converging on a general pattern here... 12218e018e9f26aa633756c9f471840945f9125c Luke Palmer lrpalmer@gmail.com e36cf61df5dcc8e678e3f4602b65ba66afc2e33a Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/31d84832cd129ac1b06c75c73169a38d8a259d35 31d84832cd129ac1b06c75c73169a38d8a259d35

2009-06-19T00:32:14-07:00

Added unfoldn and foldn conversion generators. 7b14da73e7d7e867556e71985433a3a9fc2cfb92 Luke Palmer lrpalmer@gmail.com c2c2bfaf0bcccfd126bd506c810e7a6c2c366671 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/e36cf61df5dcc8e678e3f4602b65ba66afc2e33a e36cf61df5dcc8e678e3f4602b65ba66afc2e33a

2009-06-18T22:33:00-07:00

Bugfix in convExpandLambda, and other variable-swapping conversions. 853adb4f7284f7b871e390e1fcc44cc3f2b67fa7 Luke Palmer lrpalmer@gmail.com f164795111fe36acf264332b718c9d7115dcd0df Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/c2c2bfaf0bcccfd126bd506c810e7a6c2c366671 c2c2bfaf0bcccfd126bd506c810e7a6c2c366671

2009-06-17T22:01:55-07:00

Reworking of naming conventions, stricter on folding/unfolding of symbols. 5fcaabdfd34609ab0a082885873a088b5e6dec4d Luke Palmer lrpalmer@gmail.com 3ce144094c37acd5469336e221ffefd9e85718b0 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/f164795111fe36acf264332b718c9d7115dcd0df f164795111fe36acf264332b718c9d7115dcd0df

2009-06-17T21:44:01-07:00

Added convInverseBeta, for undoing beta reductions. a28e7cd2e7c780a1d05d7f6b68ac7b7ff99bcdba Luke Palmer lrpalmer@gmail.com 1edbf2f2b3ca7129890e78ee6bdc9c67606c2576 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/3ce144094c37acd5469336e221ffefd9e85718b0 3ce144094c37acd5469336e221ffefd9e85718b0

2009-06-15T00:38:00-07:00

Fix ad-hoc naming convention. 13982dc01b24059c2eb4a88b30f696f04b2968a9 Luke Palmer lrpalmer@gmail.com df3a1da1c060c2db3f49fc2a8368ebe90008abf7 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/1edbf2f2b3ca7129890e78ee6bdc9c67606c2576 1edbf2f2b3ca7129890e78ee6bdc9c67606c2576

2009-06-15T00:28:32-07:00

Added function types. f2b104a039d976f90d5e08da9d1e64b360aadea1 Luke Palmer lrpalmer@gmail.com 2a145c1572c879e5a62a95a011cf7be4e328b5eb Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/df3a1da1c060c2db3f49fc2a8368ebe90008abf7 df3a1da1c060c2db3f49fc2a8368ebe90008abf7

2009-06-14T23:07:43-07:00

A bunch more proofs. 01b37603339400a742cdf1d6f48d34ca665ab109 Luke Palmer lrpalmer@gmail.com 733ab02ac4f61e73986b1d24c30d2e2b35324264 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/2a145c1572c879e5a62a95a011cf7be4e328b5eb 2a145c1572c879e5a62a95a011cf7be4e328b5eb

2009-06-14T22:03:12-07:00

Rename tactics to the more appropriate "prelude". (more granularity and a catalog later) 9035cb6a78d8b668bfd6381f87b297dd7d615995 Luke Palmer lrpalmer@gmail.com 1b4d766c1309a69adf110f287be9bde2fff1d192 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/733ab02ac4f61e73986b1d24c30d2e2b35324264 733ab02ac4f61e73986b1d24c30d2e2b35324264

2009-06-11T01:55:02-07:00

Woo, first proof completed! cd5584e31348ad36102d5fd9b8976f87c6506ae4 Luke Palmer lrpalmer@gmail.com 6e550dd75e8dad28dc280c52049210edd76f3011 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/1b4d766c1309a69adf110f287be9bde2fff1d192 1b4d766c1309a69adf110f287be9bde2fff1d192

2009-06-11T01:09:51-07:00

Changed to using Tactics themselves as hypotheses. 26603de6650d8556582a00919be7d0f4c56d8a81 Luke Palmer lrpalmer@gmail.com eaf863e6236e0ddf9998c4eb8576daf09cb83f3e Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/6e550dd75e8dad28dc280c52049210edd76f3011 6e550dd75e8dad28dc280c52049210edd76f3011

2009-06-11T00:57:16-07:00

Added a "prove" function to Tactic. 1d053e47906e205914e115fdfaf41ba4b9b7e29c Luke Palmer lrpalmer@gmail.com c92d34c16700225adc1d15c0fd83b0afd6ff5ce9 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/eaf863e6236e0ddf9998c4eb8576daf09cb83f3e eaf863e6236e0ddf9998c4eb8576daf09cb83f3e

2009-06-11T00:52:24-07:00

Added "theorem" tactic. c92b4f1a921e03490a236a1308a0733154bc6860 Luke Palmer lrpalmer@gmail.com f7ed462fb5268d4e97c568b6145b76a72cef2cf6 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/c92d34c16700225adc1d15c0fd83b0afd6ff5ce9 c92d34c16700225adc1d15c0fd83b0afd6ff5ce9

2009-06-11T00:47:25-07:00

Added an HOAS convenience module. 6ac8b6439cc0de206a27bc8a9a9acdb55bc0768d Luke Palmer lrpalmer@gmail.com b72cdee4f989567ae9117a01f8bda7838fda5b7c Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/f7ed462fb5268d4e97c568b6145b76a72cef2cf6 f7ed462fb5268d4e97c568b6145b76a72cef2cf6

2009-06-11T00:32:36-07:00

Added the XIH rule, an obvious conservative extension. d4a9142a2c31e2ecc4e89916340a17d7e009b825 Luke Palmer lrpalmer@gmail.com fc80b78e8578a8f24d07bd1f52dcba0a9a7e98c4 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/b72cdee4f989567ae9117a01f8bda7838fda5b7c b72cdee4f989567ae9117a01f8bda7838fda5b7c

2009-06-11T00:21:05-07:00

Add another try at the tactic module. This time significantly less clever! e8ca04c8e34eef9e8faa983ab611b9775b440a67 Luke Palmer lrpalmer@gmail.com 2545aa3adf4b8a8817fb2c73fc9b79ed31d04825 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/fc80b78e8578a8f24d07bd1f52dcba0a9a7e98c4 fc80b78e8578a8f24d07bd1f52dcba0a9a7e98c4

2009-06-10T17:24:18-07:00

Fixed another bug in embedded. faf998aa641ca1f4d5c4e88844ff324e392e85d3 Luke Palmer lrpalmer@gmail.com 9dd3d5f4019f91d78c80bf8d7b45fd64ee754937 Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/2545aa3adf4b8a8817fb2c73fc9b79ed31d04825 2545aa3adf4b8a8817fb2c73fc9b79ed31d04825

2009-06-10T17:20:47-07:00

Fixed some bugs in the embedded interpreter. 4c4262b4d3feccb3dbd25a4221a78ee6141ba0a2 Luke Palmer lrpalmer@gmail.com f2643397a5030fddb88b4e7a6e509ce473f8ee3e Luke Palmer lrpalmer@gmail.com http://github.com/luqui/dana/commit/9dd3d5f4019f91d78c80bf8d7b45fd64ee754937 9dd3d5f4019f91d78c80bf8d7b45fd64ee754937

2009-06-10T17:12:28-07:00

Added embedded unsafe interpreter. 43c0fc341feba1105c34b133c3931f187552d505 Luke Palmer lrpalmer@gmail.com