Philip Wadler
|
2a7bf78b19
|
Merge pull request #456 from mdimjasevic/prop-two-plurals
Properties: fix a double plural mistake
|
2020-01-27 10:41:35 -06:00 |
|
Philip Wadler
|
0e5a71ec1e
|
Merge pull request #457 from mdimjasevic/prop-well-typed-2
Properties: fix 'well-typed' according to issue #318
|
2020-01-26 13:23:55 -06:00 |
|
Marko Dimjašević
|
557a088c78
|
Properties: fix 'well-typed' according to issue #318
|
2020-01-26 10:26:36 +01:00 |
|
Marko Dimjašević
|
6516a5d7ba
|
Properties: fix a double plural mistake
|
2020-01-25 11:20:46 +01:00 |
|
Marko Dimjašević
|
643ff85cd0
|
Properties: visual alignment of pattern matches for M —→ N in the proof of preserve
|
2020-01-24 14:59:10 +01:00 |
|
Marko Dimjašević
|
495123979c
|
Properties: fixes an informal rule in the text for β-ƛ by using a reduction relation instead of the typing judgment
|
2020-01-22 22:28:05 +01:00 |
|
Wen Kokke
|
00bd32e7ac
|
Fixed bug in link
|
2020-01-21 20:14:09 +00:00 |
|
Wen Kokke
|
d70f12a8aa
|
Merge pull request #438 from qaisjp/patch-1
Avoid line breaks in the middle of code
|
2020-01-21 17:05:14 +00:00 |
|
Wen Kokke
|
29dc9321d8
|
Minor clarifications on exercises in Naturals and Induction.
|
2020-01-21 17:04:04 +00:00 |
|
Wen Kokke
|
0003b0465f
|
Fix #451 - mention mailing lists
|
2020-01-21 17:04:04 +00:00 |
|
Jeremy Siek
|
f6606a8ee6
|
added hint to exercise forall-x
|
2020-01-19 13:32:27 -05:00 |
|
Jeremy Siek
|
ea42753758
|
added hints to Bin-isomorphism exercise
|
2020-01-18 21:38:42 -05:00 |
|
wadler
|
435bf28a9e
|
merge
|
2020-01-14 10:26:02 -03:00 |
|
wadler
|
d770366fb4
|
added SF meetup to home page
|
2020-01-14 10:24:39 -03:00 |
|
Philip Wadler
|
d26fd33118
|
Merge pull request #450 from mdimjasevic/prop-abs-ind
Properties: fix the inductive hypothesis for lambda abstraction
|
2020-01-13 12:52:49 -03:00 |
|
Marko Dimjašević
|
776f10940d
|
Properties: fix the inductive hypothesis for lambda abstraction in the description of the proof of subst
|
2020-01-13 10:45:46 +01:00 |
|
Philip Wadler
|
a49205abd3
|
Remove redundant text
Ooops, my original edit left some redundant text.
|
2020-01-10 11:41:20 -03:00 |
|
Philip Wadler
|
170496699b
|
Merge pull request #449 from ywata/emacs-unicode
Mentioning emacs unicode command #448
|
2020-01-10 11:38:56 -03:00 |
|
Philip Wadler
|
896b2b528a
|
Further edits
I rearranged the material. It is important that control characters for arrows appear next to the description of arrows.
|
2020-01-10 11:38:28 -03:00 |
|
YASUHIKO WATANABE
|
6b8e61c1e7
|
Mention emacs commands in Unicode section.
|
2020-01-10 23:19:33 +09:00 |
|
YASUHIKO WATANABE
|
eb68d083a7
|
Mention some emacs commands.
|
2020-01-10 23:18:41 +09:00 |
|
wadler
|
1fd075440f
|
fixed error in Lists
|
2020-01-10 11:02:28 -03:00 |
|
wadler
|
77a87549f6
|
Merge branch 'dev' of github.com:plfa/plfa.github.io into dev
|
2020-01-10 10:58:58 -03:00 |
|
wadler
|
fc5f645ecb
|
added link to Nextjournal
|
2020-01-10 10:58:41 -03:00 |
|
Jeremy Siek
|
95fa648a23
|
added link to course at Indiana
|
2020-01-08 14:19:30 -05:00 |
|
Philip Wadler
|
981f7850cd
|
Merge pull request #447 from mdimjasevic/prop-swap-prf-name
Properties: rename a proof for z ≢ x
|
2020-01-06 20:19:29 -03:00 |
|
Marko Dimjašević
|
338b959f95
|
Properties: rename a proof for z ≢ x
|
2020-01-06 22:46:44 +01:00 |
|
Philip Wadler
|
6842ac170b
|
merge
|
2020-01-05 22:36:53 +00:00 |
|
Philip Wadler
|
784f99a406
|
Small changes to send-marks
|
2020-01-05 22:36:10 +00:00 |
|
Wen Kokke
|
4bcd2f4f0b
|
Travis CI deployment is broken.
|
2020-01-03 16:24:41 +00:00 |
|
Wen Kokke
|
733f1d9212
|
Fix #446
|
2020-01-03 15:56:50 +00:00 |
|
Wen Kokke
|
9f6e3125e7
|
Fixed #445
|
2020-01-03 15:24:02 +00:00 |
|
Philip Wadler
|
4d393171db
|
Merge pull request #444 from mdimjasevic/lambda-typing-inj
Lambda: fix the term in an example showing typing relation is not injective
|
2020-01-03 08:54:13 -03:00 |
|
Marko Dimjašević
|
3a3539bb77
|
Lambda: fix the term in an example showing typing relation is not injective
|
2020-01-03 08:50:22 +01:00 |
|
Philip Wadler
|
233bac8071
|
Merge pull request #443 from mdimjasevic/lambda-indent-impossible
Lambda: fix indentation for correct rendering
|
2019-12-30 01:13:24 -03:00 |
|
Marko Dimjašević
|
ed97783252
|
Lambda: fix indentation for correct rendering
|
2019-12-29 22:37:49 +01:00 |
|
Philip Wadler
|
5547b5251e
|
Merge pull request #442 from mdimjasevic/lambda-suc-con
Lambda: give the suc constructor is the text with an argument
|
2019-12-28 21:53:55 +00:00 |
|
Marko Dimjašević
|
35e66258cc
|
Lambda: make the argument name consistent with the latter text
|
2019-12-28 22:47:03 +01:00 |
|
Marko Dimjašević
|
461c574f8d
|
Lambda: give the suc constructor is the text with an argument
|
2019-12-28 22:40:02 +01:00 |
|
wadler
|
a77284a415
|
added icfp tutorial
|
2019-12-28 16:47:01 -03:00 |
|
Philip Wadler
|
98cb552b38
|
merge
|
2019-12-09 12:44:24 +00:00 |
|
Philip Wadler
|
a8eaea3e47
|
updated Exam to remove mock
|
2019-12-09 12:43:59 +00:00 |
|
Philip Wadler
|
2d2b7c7fe9
|
Merge pull request #441 from googleson78/infixr-sum
Make sum type right-associative
|
2019-12-02 13:18:33 -03:00 |
|
Georgi Lyubenov
|
ef7f95b1db
|
Make sum type right-associative
|
2019-12-02 09:49:49 +02:00 |
|
Wen Kokke
|
32a626789b
|
Fix #227
|
2019-11-29 13:16:07 +00:00 |
|
Philip Wadler
|
88ce889159
|
merge
|
2019-11-19 12:52:32 +00:00 |
|
Philip Wadler
|
fd35c7b992
|
instructions for essay
|
2019-11-19 12:51:59 +00:00 |
|
wadler
|
26ead770bf
|
added exam instructions
|
2019-11-15 11:00:44 +00:00 |
|
Philip Wadler
|
345d422605
|
added mocks
|
2019-11-15 10:55:08 +00:00 |
|
Qais Patankar
|
ddb9b75c16
|
Fix white-space breaking for multiline code blocks
|
2019-11-13 14:13:58 +00:00 |
|