wadler
|
1197d2a1d0
|
swapped names in variable lookup
|
2018-04-20 15:59:09 -03:00 |
|
wadler
|
10dcc7c76b
|
lemmas in Collections and Typed renamed
|
2018-04-20 15:47:25 -03:00 |
|
wadler
|
62219722c0
|
syntax changes to Typed
|
2018-04-20 14:45:00 -03:00 |
|
wadler
|
76d8d6bcbf
|
backup before starting work
|
2018-04-20 11:14:12 -03:00 |
|
wadler
|
2e69aaf865
|
additional tidying of Typed
|
2018-04-19 19:15:21 -03:00 |
|
wadler
|
093f3f0b83
|
tidied up Typed
|
2018-04-19 19:10:51 -03:00 |
|
wadler
|
7e60fd56b8
|
titles consistently lower case
|
2018-04-19 16:58:05 -03:00 |
|
wadler
|
3d3cd69478
|
small fixes to Collections and Typed
|
2018-04-19 16:50:36 -03:00 |
|
wadler
|
966baf98f5
|
completed more lemmas in Collections
|
2018-04-19 14:47:50 -03:00 |
|
wadler
|
a8f59134fa
|
completed some lemmas in Collections
|
2018-04-19 13:39:06 -03:00 |
|
wadler
|
6ca45f28df
|
fix to Modules
|
2018-04-19 10:05:41 -03:00 |
|
wadler
|
5de10c19e2
|
fixed typo James noted
|
2018-04-19 10:03:12 -03:00 |
|
wadler
|
1eb69a9e60
|
further work on Collections
|
2018-04-18 17:56:16 -03:00 |
|
wadler
|
c12ce5c3d9
|
started to write Modules and Collections
|
2018-04-17 19:28:17 -03:00 |
|
wadler
|
ede0c7cc1b
|
more fixes to Preface
|
2018-04-17 17:38:51 -03:00 |
|
wadler
|
715cfb7fcc
|
backups
|
2018-04-17 15:54:17 -03:00 |
|
wadler
|
94523f62b5
|
edits to Preface
|
2018-04-17 15:46:48 -03:00 |
|
wadler
|
feec229497
|
proof that substitution preserves types complete
|
2018-04-16 19:01:01 -03:00 |
|
wadler
|
910fd5b67e
|
one tiny hole left
|
2018-04-16 18:55:29 -03:00 |
|
wadler
|
1bb5412c8d
|
backup after crash
|
2018-04-16 18:11:24 -03:00 |
|
wadler
|
6fad419599
|
backup before attempted fix to Typed
|
2018-04-16 16:39:05 -03:00 |
|
wadler
|
ee889a0fba
|
a couple of more holes filled
|
2018-04-16 14:50:51 -03:00 |
|
wadler
|
a6c9b3e009
|
improved definition of fresh
|
2018-04-16 14:07:48 -03:00 |
|
wadler
|
952c1d4850
|
added Membership to strandard library in Lists
|
2018-04-15 20:11:03 -03:00 |
|
wadler
|
eb0cc40573
|
further progress on substition
|
2018-04-15 19:25:50 -03:00 |
|
wadler
|
3a910fef31
|
first draft of proof for subst with holes
|
2018-04-15 14:37:13 -03:00 |
|
wadler
|
a374c52178
|
backup morning Sun 15 Apr
|
2018-04-15 10:45:03 -03:00 |
|
wadler
|
d3c48c48e5
|
Merge branch 'master' of github.com:wenkokke/sf
No idea.
|
2018-04-15 10:44:08 -03:00 |
|
wadler
|
11d5fe279f
|
backup morning Sun 15 Apr
|
2018-04-15 10:43:50 -03:00 |
|
Wen Kokke
|
68c23ebd78
|
Fixed link to extensionality in Lists
|
2018-04-15 09:41:52 +01:00 |
|
wadler
|
80eb1aff98
|
more in Typed, less in TypedDB
|
2018-04-14 19:01:15 -03:00 |
|
wadler
|
947105aca9
|
removed extend from Typed
|
2018-04-14 16:27:55 -03:00 |
|
wadler
|
b0a2c244b0
|
Typed with extend (bad idea)
|
2018-04-14 16:16:36 -03:00 |
|
wadler
|
e6737dfb4d
|
completed type preservation for subst in Typed
|
2018-04-14 14:44:01 -03:00 |
|
wadler
|
4ae89e3ac2
|
added subst to Typed halfway through type preservation
|
2018-04-13 18:39:28 -03:00 |
|
wadler
|
0927b4ff92
|
further progress on Typed
|
2018-04-12 20:50:11 -03:00 |
|
wadler
|
5b773c88f4
|
further improvements to TypedDB
|
2018-04-12 19:08:50 -03:00 |
|
wadler
|
d19c8f5a33
|
got rid of ext in TypedDB
|
2018-04-12 18:57:26 -03:00 |
|
wadler
|
e911b2a401
|
backing up before changes to TypedDB
|
2018-04-12 18:31:11 -03:00 |
|
wadler
|
dc01c12297
|
changed index to point to Typed
|
2018-04-12 11:50:23 -03:00 |
|
wadler
|
a2dfc55577
|
changed index to point to TypedDB
|
2018-04-12 11:37:28 -03:00 |
|
wadler
|
5ae889c331
|
added TypedDB, a variant on Scoped
|
2018-04-10 18:57:21 -03:00 |
|
wadler
|
b4f79811ca
|
coded up TypedDB
|
2018-04-03 20:57:07 -03:00 |
|
wadler
|
ae7bd1f265
|
Monus
|
2018-03-27 18:09:43 -03:00 |
|
wadler
|
ee3ebd3098
|
minor changes to Prelude
|
2018-03-27 16:44:58 -03:00 |
|
wadler
|
f069c6a457
|
extra stuff
|
2018-03-27 16:19:03 -03:00 |
|
wadler
|
6e6c4a9bc2
|
added universe polymorphism to Equality
|
2018-03-27 16:14:04 -03:00 |
|
wadler
|
f7ec2acef5
|
added universe polymorphism to Equality
|
2018-03-27 16:03:24 -03:00 |
|
wadler
|
858e191639
|
making sure everything is committed
|
2018-03-22 20:46:48 -03:00 |
|
wadler
|
fb3592239d
|
update Lists, Decidable and reorganise files
|
2018-03-22 18:46:29 -03:00 |
|
wadler
|
b943785e6b
|
revised Lists
|
2018-03-20 19:49:11 -03:00 |
|
wadler
|
e188bedcc2
|
updated pairs in Negation and Quantifiers
|
2018-03-20 18:44:46 -03:00 |
|
wadler
|
242e174280
|
updated pairs in Connectives
|
2018-03-20 18:32:31 -03:00 |
|
wadler
|
b263d68c7d
|
updated pairs in Connectives
|
2018-03-20 18:32:08 -03:00 |
|
wadler
|
a647ee9f9d
|
fix to even-odd in Quantifiers
|
2018-03-20 13:47:39 -03:00 |
|
wadler
|
e1bb83225b
|
small fixes to Naturals
|
2018-03-18 20:14:52 -03:00 |
|
wadler
|
b58de9d80e
|
corrected spelling
|
2018-03-18 19:30:35 -03:00 |
|
wadler
|
cd37b8a2ce
|
finished Quantifiers (again)
|
2018-03-18 19:13:27 -03:00 |
|
wadler
|
63f65333e3
|
added mention of Sigma to Quantifiers
|
2018-03-18 13:09:38 -03:00 |
|
wadler
|
8b7519220f
|
completed pass over Quantifiers
|
2018-03-18 12:27:39 -03:00 |
|
wadler
|
d878b55f2e
|
extra files for even exists proofs
|
2018-03-17 21:17:48 -03:00 |
|
wadler
|
9ed10c3d29
|
fix to Decidable and related extra files
|
2018-03-17 17:30:58 -03:00 |
|
wadler
|
6f5c8d2330
|
small fixes to all files
|
2018-03-17 15:09:15 -03:00 |
|
wadler
|
752f34c9e5
|
saving before lunch
|
2018-03-17 13:23:15 -03:00 |
|
wadler
|
83776712ac
|
added unequal to Negation
|
2018-03-17 12:27:07 -03:00 |
|
wadler
|
81b5da1ebd
|
moving LogicAns to NegationAns
|
2018-03-17 11:51:09 -03:00 |
|
wadler
|
29ed7cdbeb
|
halfway through Quantifiers
|
2018-03-15 19:08:31 -03:00 |
|
wadler
|
77ebd9b67f
|
added Devil story to Negation
|
2018-03-15 13:02:32 -03:00 |
|
wadler
|
f3fa5ff5fd
|
end material for Connectives
|
2018-03-15 11:47:49 -03:00 |
|
wadler
|
72ed3ad3d9
|
fixed bug in Lists
|
2018-03-15 11:11:08 -03:00 |
|
wadler
|
18dd52b4d0
|
got Negation and Quantification to compile
|
2018-03-15 10:38:44 -03:00 |
|
wadler
|
b31d8eba50
|
fixed bug in Connectives
|
2018-03-14 18:34:46 -03:00 |
|
wadler
|
771bd2de5d
|
removed Connectives-old, updated index
|
2018-03-14 18:32:44 -03:00 |
|
wadler
|
ef062ba226
|
added eta to Connectives, added Negation and Quantifiers
|
2018-03-14 18:31:30 -03:00 |
|
wadler
|
2e2ebb5665
|
updating Connectives, finishing exponentials
|
2018-03-13 18:59:10 -03:00 |
|
wadler
|
bbee34baa2
|
revised up through Isomorphism
|
2018-03-13 13:24:22 -03:00 |
|
wadler
|
65e6af9d4b
|
revisions on Natural to Isomorphism
|
2018-03-12 19:33:13 -03:00 |
|
wadler
|
0ba37f5fb4
|
first pass over Isomorphism
|
2018-03-12 18:02:41 -03:00 |
|
wadler
|
63a38ec261
|
added various files in extra
|
2018-03-12 13:04:51 -03:00 |
|
wadler
|
926558bfe6
|
completed pass over Equality
|
2018-03-12 13:01:08 -03:00 |
|
wadler
|
dffb291510
|
completed pass over Equality
|
2018-03-12 12:53:30 -03:00 |
|
wadler
|
c90f0f9af0
|
fiddling with Equality
|
2018-03-11 18:52:48 -03:00 |
|
wadler
|
b191d639c8
|
updated RelationsAns
|
2018-03-08 18:44:26 -03:00 |
|
wadler
|
1ff0d97564
|
revised Relations, further fixes
|
2018-03-08 18:04:38 -03:00 |
|
wadler
|
c05e9b49ed
|
revised Relations
|
2018-03-08 17:15:01 -03:00 |
|
wadler
|
6538feeda5
|
completed revision of Relations
|
2018-03-07 18:13:11 -03:00 |
|
wadler
|
67689be194
|
fixed import at end of Properties
|
2018-03-07 17:40:56 -03:00 |
|
wadler
|
ee13c1c6ed
|
halfway through Relations
|
2018-03-07 13:25:35 -03:00 |
|
wadler
|
b088ee59cf
|
tiny fix to Properties
|
2018-03-07 11:55:29 -03:00 |
|
wadler
|
ea44518e27
|
fix to RelationsAns
|
2018-03-06 18:38:27 -03:00 |
|
wadler
|
bcc8e78eb4
|
completed revisions of Naturals and Properties
|
2018-03-06 18:18:05 -03:00 |
|
wadler
|
5f738df949
|
first rewrite of assoc and comm
|
2018-03-06 15:34:15 -03:00 |
|
wadler
|
73ab7f0dc0
|
removed Typed, which is redundant
|
2018-03-05 19:02:10 -03:00 |
|
wadler
|
dbd5399b85
|
further revisions to Properties
|
2018-03-05 19:00:21 -03:00 |
|
wadler
|
929da32c56
|
further revisions to Naturals
|
2018-03-05 18:34:22 -03:00 |
|
wadler
|
a6f413ecb4
|
changed examples in Naturals
|
2018-03-05 13:25:56 -03:00 |
|
wadler
|
61d00be7c1
|
further fixes to Preface, Acknowledgements
|
2018-03-04 17:59:36 -03:00 |
|
wadler
|
62c6e88b14
|
fix to Preface, Acknowledgements
|
2018-03-04 17:43:16 -03:00 |
|
wadler
|
fb3ad1d4bd
|
small fixes to Preface, about, index
|
2018-03-04 12:37:40 -03:00 |
|
wadler
|
ae26e82dd4
|
wrote Preface
|
2018-03-04 12:29:53 -03:00 |
|
wadler
|
d2c64685db
|
added Notes
|
2018-03-04 10:57:27 -03:00 |
|
wadler
|
6e6531e7ae
|
minor change to Naturals
|
2018-03-01 20:27:15 +01:00 |
|
wadler
|
e34252934f
|
revised text of Naturals
|
2018-03-01 20:23:54 +01:00 |
|
wadler
|
0afaa0aa3a
|
added imports to Naturals
|
2018-03-01 18:47:32 +01:00 |
|
wadler
|
d9a79cf298
|
Revised Natural
|
2018-02-27 18:45:52 +01:00 |
|
wadler
|
c4ae7c86bc
|
added PHOAS to Scoped
|
2018-02-27 17:49:33 +01:00 |
|
wadler
|
e739cd7029
|
added letters to repository
|
2018-02-27 17:24:58 +01:00 |
|
wadler
|
45a4be4fa6
|
small fix to Typed
|
2018-02-27 14:54:22 +01:00 |
|
wadler
|
4e4fc99920
|
changed DeBruijn to Scoped
|
2018-02-27 14:50:21 +01:00 |
|
wadler
|
11e9a4e99d
|
removed hole from DeBruijn
|
2018-02-26 12:18:29 +01:00 |
|
wadler
|
178c0f8dc4
|
updating DeBruijn for PHOAS
|
2018-02-26 09:09:43 +01:00 |
|
wadler
|
657feddf46
|
moved DeBruijn to src so it will be published
|
2018-02-24 19:50:20 +01:00 |
|
wadler
|
b453ef1efc
|
completed progress
|
2018-02-24 17:32:51 +01:00 |
|
wadler
|
edfbdd1a0d
|
halfway through DeBruijn
|
2018-02-24 16:31:35 +01:00 |
|
wadler
|
b0226ccb41
|
halfway through DeBruijn
|
2018-02-24 13:45:45 +01:00 |
|
wadler
|
543017049d
|
added Darais
|
2018-02-23 14:50:29 +01:00 |
|
wadler
|
c75cd9dc06
|
further work on DeBruijn
|
2018-02-23 13:45:53 +01:00 |
|
wadler
|
ea08e95665
|
restored original DeBruijn
|
2018-02-22 12:53:22 +01:00 |
|
wadler
|
3391c18b53
|
second order DeBruijn
|
2018-02-22 12:51:16 +01:00 |
|
wadler
|
f6f41167ba
|
Stable and DeBruijn
|
2018-02-20 12:42:19 +01:00 |
|
wadler
|
2a45baba90
|
Decidable All
|
2018-02-18 12:40:59 -03:00 |
|
wadler
|
151dc6d6bd
|
Decidable connectives
|
2018-02-18 11:08:20 -03:00 |
|
wadler
|
32a2062a78
|
added Everything
|
2018-02-16 17:30:23 -02:00 |
|
wadler
|
f97bac1082
|
Decidable, first half
|
2018-02-16 17:08:58 -02:00 |
|
wadler
|
a6e1179622
|
minor fixes to Lists
|
2018-02-15 09:40:27 -02:00 |
|
wadler
|
f939eebf5b
|
fixed bug in LogicAns
|
2018-02-14 21:10:07 -02:00 |
|
wadler
|
9114aad7b3
|
finished first draft of Lists
|
2018-02-14 20:14:54 -02:00 |
|
wadler
|
652da6c516
|
Lists, added All and Any
|
2018-02-14 19:34:10 -02:00 |
|
wadler
|
462a88508f
|
finished Lists foldr monoid
|
2018-02-12 15:17:48 -02:00 |
|
wadler
|
ab9e5d6c7d
|
Revised material on sections
|
2018-02-09 15:27:31 -04:00 |
|
wadler
|
9c3a362a62
|
Lists, map and fold
|
2018-02-08 17:41:51 -04:00 |
|
wadler
|
2871611bec
|
updated Agda
|
2018-02-08 14:31:35 -04:00 |
|
wadler
|
2e93d44877
|
Lists, up through fast reverse
|
2018-02-07 14:17:56 -04:00 |
|
wadler
|
e37d1692c9
|
added ListsAns
|
2018-02-07 11:46:48 -04:00 |
|
wadler
|
8011389aa9
|
append, length, reverse in Lists
|
2018-02-06 16:57:35 -04:00 |
|
wadler
|
e5d6f95e77
|
started text for Lists
|
2018-02-05 17:58:51 -04:00 |
|
wadler
|
65572ed522
|
Lists
|
2018-02-04 18:06:41 -04:00 |
|
wadler
|
4df09d9b05
|
code for Lists
|
2018-01-31 21:26:08 -02:00 |
|
wadler
|
650610600f
|
added tabular reasoning for embedding
|
2018-01-31 16:57:11 -02:00 |
|
wadler
|
871573291a
|
refactoring of Isomorphsim complete
|
2018-01-31 16:49:53 -02:00 |
|
wadler
|
e39a019602
|
factored out Isomorphism, Logic broken
|
2018-01-31 12:53:08 -02:00 |
|
wadler
|
dd021129f2
|
finished rewriting about to start Leibniz
|
2018-01-31 10:20:37 -02:00 |
|
wadler
|
27b038de35
|
backing up Equivalence
|
2018-01-31 09:30:41 -02:00 |
|
wadler
|
465594f495
|
starting to explain rewrite
|
2018-01-30 18:59:52 -02:00 |
|
wadler
|
185d8981f0
|
added explanation of tabular reasoning
|
2018-01-30 17:58:57 -02:00 |
|
wadler
|
b0d7c5f49c
|
halfway through Equivalence
|
2018-01-29 21:01:19 -02:00 |
|
wadler
|
00b156f6cb
|
Fixed PropertiesAns and RelationsAns
|
2018-01-28 18:42:55 +00:00 |
|
wadler
|
b93d1168be
|
Cherry-picked cleanup of logic intro to master
|
2018-01-28 18:29:38 +00:00 |
|
wadler
|
f195408df4
|
test --- does change push?
|
2018-01-28 15:35:14 -02:00 |
|
wadler
|
6cadf407e4
|
shifting to main branch as suggested by Wen
|
2018-01-28 15:31:18 -02:00 |
|
wadler
|
71d92c3776
|
redid comm, even exists proof
|
2018-01-26 19:36:31 -02:00 |
|
wadler
|
6ae06a2236
|
further progress on Logic
|
2018-01-26 19:35:55 -02:00 |
|
wadler
|
7c68837152
|
drafted universals and existentials
|
2018-01-26 17:02:51 -02:00 |
|
wadler
|
4e0aeabfe4
|
Publishing draft of Logic
|
2018-01-26 14:37:46 -02:00 |
|
wadler
|
005f007543
|
Logic prior to universals
|
2018-01-26 14:13:09 -02:00 |
|
wadler
|
c8779277f6
|
further work on Logic
|
2018-01-23 13:52:55 +00:00 |
|
wadler
|
f1e3b44cff
|
Logic, true, false, negation
|
2018-01-14 19:51:42 +00:00 |
|
wadler
|
28d971a886
|
Logic, currying and related isos
|
2018-01-12 19:31:59 -02:00 |
|
wadler
|
5d767f5b40
|
Logic, currying and related isos
|
2018-01-12 19:10:46 -02:00 |
|
wadler
|
b60bc9a8d8
|
Logic, embedding
|
2018-01-12 17:20:52 -02:00 |
|
wadler
|
26c63340e8
|
mutual recursion
|
2018-01-12 15:37:26 -02:00 |
|
wadler
|
64dc1651c3
|
added Mutual
|
2018-01-11 13:27:33 -02:00 |
|
wadler
|
390816ea97
|
updated Logic, added extra Gentzen
|
2018-01-10 19:42:25 -02:00 |
|
wadler
|
ab8c9aa7aa
|
trying to prove distribution
|
2018-01-09 20:08:39 -02:00 |
|
wadler
|
bc9cd1934a
|
trying to prove distribution
|
2018-01-09 20:05:52 -02:00 |
|
wadler
|
3d919975fa
|
added material on isomorphism to Logic
|
2018-01-09 19:54:08 -02:00 |
|
wadler
|
cf7a6b5c56
|
added trial of Reasoning
|
2018-01-09 14:45:11 -02:00 |
|
wadler
|
7d516c8a9f
|
added Logic
|
2018-01-05 21:30:39 -02:00 |
|
wadler
|
62f3ccd3bd
|
PropertiesEx and RelationsEx
|
2018-01-05 19:30:53 -02:00 |
|
wadler
|
75f59e722d
|
created EvenOdd
|
2018-01-05 19:29:29 -02:00 |
|
wadler
|
e43a20aa2e
|
created RelationsEx
|
2018-01-05 19:18:21 -02:00 |
|
wadler
|
0e4c77c0fb
|
renaming to match standard library
|
2018-01-05 14:07:31 -02:00 |
|
wadler
|
2fc99f5b5d
|
finished first draft of Relations save for exercises
|
2018-01-04 20:43:26 -02:00 |
|
wadler
|
c9a71c9631
|
finished totality
|
2018-01-04 19:51:00 -02:00 |
|
wadler
|
f1d4946613
|
starting on antisymmetry
|
2018-01-04 13:23:15 -02:00 |
|
wadler
|
8eb3f00554
|
text for reflexivity and transitivity
|
2018-01-04 12:37:25 -02:00 |
|
wadler
|
8f6f629ff2
|
added Relations
|
2018-01-03 20:03:08 -02:00 |
|
wadler
|
85312c0f00
|
added Exercises
|
2018-01-02 19:47:04 -02:00 |
|
wadler
|
db395b3d89
|
completed first draft of Properties save for exercises
|
2018-01-02 18:15:13 -02:00 |
|
wadler
|
33640cf86e
|
fixing ndash and mdash
|
2018-01-01 19:03:51 -02:00 |
|
wadler
|
bf6c5a0602
|
finished proof of assoc+
|
2018-01-01 17:40:30 -02:00 |
|
wadler
|
7c7ecbe950
|
added Properties
|
2018-01-01 15:45:01 -02:00 |
|
wadler
|
d83f9539a1
|
finished with Induction for Sunday@
|
2017-12-31 13:09:53 -02:00 |
|
wadler
|
cc1eb04846
|
clean up
|
2017-12-31 11:55:06 -02:00 |
|
wadler
|
2800de86e3
|
completed subsection on recursive definitions
|
2017-12-30 14:48:32 -02:00 |
|
wadler
|
76e9b8e690
|
completed subsection on recursive definitions
|
2017-12-30 14:38:09 -02:00 |
|
wadler
|
4c538c96dd
|
inductive definition of addition
|
2017-12-30 12:54:51 -02:00 |
|
wadler
|
bd3e2762aa
|
starting second section of Naturals
|
2017-12-30 11:35:29 -02:00 |
|
wadler
|
92efda2162
|
minor edits to Natural. End of work on Fri 29 Dec
|
2017-12-29 15:58:21 -02:00 |
|
wadler
|
1bd1f19f52
|
added more to Naturals
|
2017-12-29 15:53:02 -02:00 |
|
wadler
|
5d4997bc0c
|
fixed index
|
2017-12-29 14:56:08 -02:00 |
|
wadler
|
a83e020034
|
first draft of Naturals
|
2017-12-29 14:54:12 -02:00 |
|
Philip Wadler
|
3f10630ab8
|
refinements to Basics
|
2017-10-03 12:59:23 +01:00 |
|
Philip Wadler
|
964ed65922
|
decidable equality in basics
|
2017-10-01 22:06:35 +01:00 |
|
Philip Wadler
|
4d04279d04
|
a bit more basics of arithmetic
|
2017-10-01 21:46:17 +01:00 |
|
Philip Wadler
|
9067c7a317
|
basics of arithmetic
|
2017-10-01 21:36:21 +01:00 |
|
Philip Wadler
|
6ff8e77c22
|
changes to README and config
|
2017-09-13 17:34:32 +01:00 |
|
wadler
|
844d39fef0
|
added unicode names
|
2017-07-24 12:05:21 +01:00 |
|
wadler
|
a96c961727
|
added emoji example to alpha renaming
|
2017-07-24 11:54:46 +01:00 |
|
Philip Wadler
|
8fb67556ed
|
last fixes to Stlc and StlcProp before sending out for comment
|
2017-07-19 13:02:23 +01:00 |
|
Philip Wadler
|
b0a6f9bc5a
|
small fix to Stlc
|
2017-07-17 18:12:41 +01:00 |
|
Philip Wadler
|
4c5214b882
|
small fix to Stlc
|
2017-07-17 18:11:44 +01:00 |
|
Philip Wadler
|
8658bb1b42
|
finished first draft of Stlc
|
2017-07-17 18:09:37 +01:00 |
|
Philip Wadler
|
3b62e81c06
|
minor fixes to Stlc
|
2017-07-17 16:06:36 +01:00 |
|
Philip Wadler
|
b66ccb4dd6
|
added material on free and bound variables to Stlc
|
2017-07-14 18:42:45 +01:00 |
|
Philip Wadler
|
1738eb3998
|
first draft of Stlc complete to beginning of types
|
2017-07-14 17:30:05 +01:00 |
|
Philip Wadler
|
daf8cda196
|
starting on values
|
2017-07-14 14:25:34 +01:00 |
|
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
|
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
|
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 |
|
wadler
|
ec46d635c0
|
inductive data type for progress
|
2017-06-29 23:05:23 +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 |
|
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 |
|
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 |
|
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 |
|
wadler
|
10214fef6c
|
completed progress
|
2017-06-23 13:10:30 +01:00 |
|
wadler
|
1b6e887f05
|
fixing up versions
|
2017-06-23 11:11:14 +01:00 |
|
wadler
|
66132f1dbb
|
added StlcPropOld
|
2017-06-23 11:09:29 +01:00 |
|
Wen Kokke
|
b4e3fe6302
|
Edited Maps
|
2017-06-21 17:00:34 +02:00 |
|
Wen Kokke
|
1c9b86fb26
|
Finished implementing Maps
|
2017-06-21 16:59:10 +02:00 |
|
wadler
|
c1c997589d
|
restored Id to String
|
2017-06-20 20:56:44 +01:00 |
|
wadler
|
91fb356db0
|
fixed problem in Maps
|
2017-06-20 20:48:54 +01:00 |
|
wadler
|
f639060d7c
|
restored MapsOld for purposes of comparison
|
2017-06-20 19:57:05 +01:00 |
|
wadler
|
f496e55e7c
|
completed first draft of Stlc
|
2017-06-20 17:17:33 +01:00 |
|
wadler
|
f5fca1e270
|
small cleanup to standard library
|
2017-06-20 15:16:50 +01:00 |
|
wadler
|
ab6da37b16
|
documented problem with holes
|
2017-06-20 14:44:15 +01:00 |
|
wadler
|
65d9e7cdfd
|
updated Maps
|
2017-06-20 14:35:24 +01:00 |
|
wadler
|
43b46ef775
|
updated Maps
|
2017-06-20 14:20:47 +01:00 |
|
wadler
|
e6199666b0
|
changed unicode := to ascii
|
2017-06-19 20:11:58 +01:00 |
|
wadler
|
196c2f44ce
|
Moved Stlc to StlcOld, replace Stlc by Phil's version
|
2017-06-19 19:44:37 +01:00 |
|
Pepijn Kokke
|
b24f041240
|
Corrected links in Maps.
|
2017-03-11 23:57:16 +00:00 |
|
Pepijn Kokke
|
d5a9a6345a
|
Regenerated files after bug-fix in agda2html.
|
2017-03-11 23:53:35 +00:00 |
|
Pepijn Kokke
|
f96b046cbc
|
Moved imports up to the top of the file in all files except for Maps. Created clean and clobber tasks.
|
2017-03-11 23:07:56 +00:00 |
|
Pepijn Kokke
|
a7cecb2b23
|
Minor changes in existing modules.
|
2017-03-11 23:00:02 +00:00 |
|
Pepijn Kokke
|
f58de1fcdc
|
Worked on the layout.
|
2017-03-11 22:28:50 +00:00 |
|
Pepijn Kokke
|
f682a4c8d7
|
Merge branch 'master' of github.com:pepijnkokke/sf
* 'master' of github.com:pepijnkokke/sf:
updated stlc
|
2017-03-10 16:03:16 +00:00 |
|
Pepijn Kokke
|
64cb6da7c8
|
Rerendered and reorganized the *.md files; removed junk; centered equations.
|
2017-03-10 16:02:07 +00:00 |
|
Pepijn Kokke
|
21b52e98e4
|
Moved .lagda files into src/; added basic structure of a website.
|
2017-03-10 15:49:30 +00:00 |
|