wadler
|
9171a5c632
|
add pdf
|
2020-03-10 11:17:07 -03:00 |
|
Jeremy Siek
|
7e514800eb
|
improved some proofs
|
2020-03-10 09:44:41 -04:00 |
|
Jeremy Siek
|
0a94cddd2f
|
changed name of lemma
|
2020-03-09 16:14:24 -04:00 |
|
wadler
|
de8c6ae3ef
|
merge
|
2020-03-04 19:16:36 -03:00 |
|
wadler
|
6300a449ff
|
revision of scp paper
|
2020-03-04 19:16:18 -03:00 |
|
Wen Kokke
|
134b06dbe1
|
Merge pull request #467 from moleike/patch-2
fix typo
|
2020-02-20 12:55:00 +00:00 |
|
Alexandre Moreno
|
6f27a9b7e6
|
fix typo
|
2020-02-20 13:10:04 +08:00 |
|
Jeremy Siek
|
dc7da4961b
|
fixed typo
|
2020-02-19 15:59:44 -05:00 |
|
wadler
|
4df3cb67a1
|
merge
|
2020-02-14 10:36:20 -03:00 |
|
wadler
|
ea6483024e
|
added Adrian's comments to Notes.md
|
2020-02-14 10:35:49 -03:00 |
|
Wen Kokke
|
a8b53353a7
|
Merge pull request #465 from MatthiasGabriel/patch-2
Remove strange line break
|
2020-02-13 14:48:58 +00:00 |
|
Matthias Gabriel
|
747998cd63
|
Remove strange line break
Remove a strange line break in the middle of the formula. I guess the mark-down respects that line break because it's part of the formula.
|
2020-02-13 15:46:39 +01:00 |
|
Wen Kokke
|
10bfcebc44
|
Merge pull request #464 from MatthiasGabriel/typo/begriffsschrift
Correct wrong book title
|
2020-02-13 12:32:39 +00:00 |
|
Matthias Gabriel
|
e2916d7642
|
Update Naturals.lagda.md
Correct wrong title. The book is called Begriffsschrift.
|
2020-02-13 12:49:51 +01:00 |
|
Jeremy Siek
|
f3fa4feb95
|
simpler hint for Bin-isomorphism
|
2020-02-11 15:50:30 -05:00 |
|
Wen Kokke
|
1c06cd319d
|
Merge pull request #463 from plfa/zachrbrown-dev
Minor changes to fix #460
|
2020-02-08 14:32:04 +00:00 |
|
Wen Kokke
|
84556ab62e
|
Minor fix
|
2020-02-08 14:30:29 +00:00 |
|
Wen Kokke
|
aaaabb1a20
|
Merge pull request #462 from fangyi-zhou/anchors
Use anchorjs for generating anchors
|
2020-02-08 14:27:39 +00:00 |
|
Fangyi Zhou
|
f4776a9df4
|
Use anchorjs for generating anchors
|
2020-02-07 23:31:20 +00:00 |
|
Zachary Brown
|
310ab57692
|
Address PR feedback — remove additional agda specifics
|
2020-02-06 17:04:02 -08:00 |
|
Jeremy Siek
|
7c1d4d7903
|
added to the hint
|
2020-02-01 14:36:58 -05:00 |
|
Zachary Brown
|
25fbc53ecb
|
Add note about agda pragma placement
|
2020-01-29 16:02:46 -08:00 |
|
Philip Wadler
|
c50f5713bc
|
Merge pull request #458 from mdimjasevic/denot-untyped-to
Denotational semantics: remove a double 'to'
|
2020-01-27 15:27:38 -06:00 |
|
Jeremy Siek
|
eae2f16659
|
fix a typo
|
2020-01-27 16:18:00 -05:00 |
|
Philip Wadler
|
83b8e6da00
|
Merge pull request #452 from mdimjasevic/prop-preserve-beta
Properties: fix an informal rule in the text for β-ƛ
|
2020-01-27 14:59:33 -06:00 |
|
Marko Dimjašević
|
8aff938f71
|
Denotational: remove a double 'to'
|
2020-01-27 21:42:17 +01:00 |
|
Philip Wadler
|
d7143136ef
|
Merge pull request #453 from mdimjasevic/prop-vis-align
Properties: visual alignment of pattern matches for M —→ N
|
2020-01-27 14:09:47 -06:00 |
|
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 |
|