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 |
|