wadler
|
6d97cb0101
|
fix typo
|
2020-03-31 08:34:37 -03:00 |
|
Jeremy Siek
|
14b1fb0e10
|
fix formatting
|
2020-03-30 16:21:48 -04:00 |
|
Jeremy Siek
|
2412de33fc
|
Merge branch 'dev' of https://github.com/plfa/plfa.github.io into dev
|
2020-03-30 15:57:31 -04:00 |
|
Jeremy Siek
|
850de4b860
|
fix typo
|
2020-03-30 15:57:23 -04:00 |
|
wadler
|
07f33fd85d
|
merge
|
2020-03-30 09:07:19 -03:00 |
|
wadler
|
805f1fd31a
|
updated name
|
2020-03-30 09:06:53 -03:00 |
|
wadler
|
dacd7c9d78
|
added SCP final version
|
2020-03-30 09:05:58 -03:00 |
|
Jeremy Siek
|
8ffc49e929
|
minor text edit
|
2020-03-29 16:53:38 -04:00 |
|
Jeremy Siek
|
2486155f3f
|
doh! got Church and Scott mixed up, unfixing
|
2020-03-29 16:51:25 -04:00 |
|
Jeremy Siek
|
6dc437bce7
|
new exercise
|
2020-03-28 16:23:56 -04:00 |
|
Jeremy Siek
|
e51e255d8d
|
fixed suc_
|
2020-03-27 11:35:26 -04:00 |
|
Jeremy Siek
|
724ec85423
|
substZero
|
2020-03-25 15:42:33 -04:00 |
|
Jeremy Siek
|
8ef93f790b
|
fixed hint
|
2020-03-25 15:25:59 -04:00 |
|
wadler
|
639b903670
|
merge
|
2020-03-12 16:46:12 -03:00 |
|
wadler
|
460c87eeaa
|
update pdf
|
2020-03-12 16:45:54 -03:00 |
|
Jeremy Siek
|
6ef39138b7
|
minor edits
|
2020-03-11 16:08:04 -04:00 |
|
Jeremy Siek
|
08508f9e36
|
renamed dom and cod
|
2020-03-11 15:55:44 -04:00 |
|
Jeremy Siek
|
6b595851d6
|
another tweak
|
2020-03-11 15:45:02 -04:00 |
|
Jeremy Siek
|
552ec893c6
|
tweak
|
2020-03-11 13:47:25 -04:00 |
|
Jeremy Siek
|
7acc69d836
|
minor edit
|
2020-03-11 13:44:46 -04:00 |
|
Jeremy Siek
|
1c54d99cbe
|
an example got out of sync with the text
|
2020-03-11 13:35:52 -04:00 |
|
Jeremy Siek
|
40f287e050
|
removed remaining references to nth
|
2020-03-11 13:26:56 -04:00 |
|
wadler
|
489daa4519
|
merge
|
2020-03-10 11:17:31 -03:00 |
|
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 |
|