Philip Wadler
|
0a824e8e03
|
finished syntax
|
2017-07-14 12:05:59 +01:00 |
|
Philip Wadler
|
f949776082
|
syntax examples
|
2017-07-14 11:26:50 +01:00 |
|
Philip Wadler
|
aef1fa75ca
|
finished intro to syntax
|
2017-07-14 11:07:38 +01:00 |
|
Philip Wadler
|
626d87804f
|
merging informal description with bnf
|
2017-07-14 11:02:44 +01:00 |
|
Philip Wadler
|
5b63add070
|
fixed symbol for numeric constants
|
2017-07-14 10:59:03 +01:00 |
|
Philip Wadler
|
a43bdb46c7
|
fixed backticks in code spans
|
2017-07-14 10:56:59 +01:00 |
|
Philip Wadler
|
3de139a5ef
|
partway through syntax of Stlc
|
2017-07-13 17:02:56 +01:00 |
|
Philip Wadler
|
4ea1d650a8
|
introduction for Stlc
|
2017-07-12 17:14:37 +01:00 |
|
Philip Wadler
|
4da22ebb55
|
finished first pass of StlcProp
|
2017-07-12 16:25:49 +01:00 |
|
Philip Wadler
|
2f1f78d8b3
|
fit to available space
|
2017-07-12 15:52:31 +01:00 |
|
Philip Wadler
|
a2940a3b12
|
renaming
|
2017-07-12 15:47:22 +01:00 |
|
Philip Wadler
|
53aaa1e3fc
|
publish html
|
2017-07-11 17:58:04 +01:00 |
|
Philip Wadler
|
728e54cc83
|
completed soundness
|
2017-07-11 17:57:24 +01:00 |
|
Philip Wadler
|
32307b9e4b
|
fire alarm
|
2017-07-11 17:22:11 +01:00 |
|
Philip Wadler
|
929400d012
|
updated StlcProp through end of preservation
|
2017-07-11 15:16:23 +01:00 |
|
Philip Wadler
|
c059b831af
|
continuing to revise Stlc and StlcProp
|
2017-07-11 13:55:00 +01:00 |
|
wadler
|
eceafb86eb
|
pushing html
|
2017-07-06 23:13:06 +01:00 |
|
wadler
|
020fed2395
|
tried out C-c C-a
|
2017-07-06 23:12:06 +01:00 |
|
Philip Wadler
|
a50ccd7315
|
revised StlcProp up to start of Substitution
|
2017-07-04 18:38:18 +01:00 |
|
Philip Wadler
|
31aece1144
|
revising Stlc and StlcProp
|
2017-07-04 18:33:27 +01:00 |
|
Philip Wadler
|
121c247f43
|
better Agda support for computing reductions
|
2017-07-04 17:49:20 +01:00 |
|
Philip Wadler
|
04b9184312
|
updated
|
2017-07-04 12:59:55 +01:00 |
|
wadler
|
ec46d635c0
|
inductive data type for progress
|
2017-06-29 23:05:23 +01:00 |
|
wadler
|
5c02a1a5cb
|
updated instructions in README
|
2017-06-29 16:43:38 +01:00 |
|
wadler
|
3f9fc08a35
|
preparing to publish
|
2017-06-29 15:18:10 +01:00 |
|
wadler
|
2c6d88c3ee
|
checked derivations work with C-R
|
2017-06-29 14:59:37 +01:00 |
|
wadler
|
2cf5421261
|
updated derivations in Stlc
|
2017-06-29 14:01:44 +01:00 |
|
wadler
|
04797f1632
|
backed up Preorder
|
2017-06-29 12:55:49 +01:00 |
|
wadler
|
76fc4a55c2
|
updated StlcProp to new syntax
|
2017-06-28 17:44:16 +01:00 |
|
wadler
|
36e38db1fc
|
updated Stlc to new syntax
|
2017-06-28 17:24:16 +01:00 |
|
wadler
|
a5646aa559
|
minor changes
|
2017-06-28 15:12:53 +01:00 |
|
Wen Kokke
|
dec8fd5705
|
Expanded Makefile -- regenerated outputs.
|
2017-06-27 16:10:16 +01:00 |
|
Philip Wadler
|
6c4fa4bf72
|
twiddled imports for PreorderReasoning
|
2017-06-27 15:52:07 +01:00 |
|
Wen Kokke
|
ba15881340
|
Started rewriting with Reasoning notation
|
2017-06-27 15:47:46 +01:00 |
|
Wen Kokke
|
bc1fb14431
|
Started rewriting with Reasoning notation
|
2017-06-27 15:42:04 +01:00 |
|
Wen Kokke
|
eaeab73fc1
|
Re-regenerated the output files
|
2017-06-27 15:25:04 +01:00 |
|
Philip Wadler
|
9071f42d41
|
publish
|
2017-06-27 14:58:07 +01:00 |
|
Wen Kokke
|
dc4c1bce16
|
Remove all *Old.lagda files
|
2017-06-27 14:57:24 +01:00 |
|
Wen Kokke
|
7b804c29b5
|
Added make serve task to the Makefile
|
2017-06-27 14:54:09 +01:00 |
|
Philip Wadler
|
77390abcc9
|
publish
|
2017-06-27 14:22:52 +01:00 |
|
Philip Wadler
|
b9b05b1347
|
first complete draft of StlcProp
|
2017-06-27 13:56:56 +01:00 |
|
wadler
|
cb27a230c8
|
further improvements to StlcProp, only two holes left
|
2017-06-26 13:38:08 +01:00 |
|
wadler
|
3da3cdb235
|
updated Maps with extensionality
|
2017-06-26 13:16:13 +01:00 |
|
wadler
|
949c48b206
|
finished preservation, renamed substitution, substitution preservation still to do
|
2017-06-26 11:22:36 +01:00 |
|
wadler
|
fbd3cc1d2e
|
stuck at two places in proof of preservation of substitution
|
2017-06-25 19:09:39 +01:00 |
|
wadler
|
500d56b3b0
|
stuck at two places in proof of preservation of substitution
|
2017-06-25 19:08:11 +01:00 |
|
wadler
|
6ee9d8dd40
|
halfway through preservation of substitution
|
2017-06-25 16:40:10 +01:00 |
|
wadler
|
fe5bf01e6b
|
added example reductions to Stlc
|
2017-06-25 00:03:10 +01:00 |
|
wadler
|
fa627864e0
|
added weakening to StlcProp
|
2017-06-23 18:20:49 +01:00 |
|
wadler
|
62cb6c064a
|
partway through StlcProp
|
2017-06-23 17:17:51 +01:00 |
|