Wen Kokke
6bc9ccd609
Fix #488
2020-07-08 11:10:15 +01:00
Wen Kokke
6edc6e5b85
Fix #487
2020-07-02 13:06:24 +01:00
Wen Kokke
353ff35644
Merge pull request #485 from mreed20/epubcheck
...
Fix remaining epubcheck warnings
2020-07-02 10:17:27 +01:00
Michael Reed
024a62d29f
Fix remaining epubcheck warnings
...
HTML does not permit nested <p> elements, which epubcheck complains
about. This change fixes those remaining warnings.
This change also causes the Dedication on the website to be centered
when viewed in Safari, which it was not before. The EPUB output looks
the same in either version with Thorium reader 1.3 on macOS.
2020-06-28 20:28:46 -04:00
Michael Reed
99aa26401f
EPUB: Populate acknowledgements.md with contributors
...
Use liquid-lua to generate acknowledgements_epub.md, which is used by
pandoc to build the EPUB book. Also stop using the '{%-' / '-%}'
syntax, which liquid-lua does not support, in templates.
Also add a vertical space between the first bullet in each bulleted
list so pandoc recognizes bulleted lists as such. This has no effect on
the the website.
2020-06-28 14:17:45 -04:00
Wen Kokke
80ba7fdfec
Changed acknowledgements.
2020-06-19 13:53:29 +01:00
Wen Kokke
f1296fbd3b
Changed acknowledgements.
2020-06-19 13:40:29 +01:00
Wen Kokke
1d4913d89f
Fix Dedication.
2020-06-18 12:33:18 +01:00
Wen Kokke
8469ed41cb
Changed layout in Dedication.
2020-06-18 08:26:47 +01:00
Michael Reed
75654740b3
EPUB: Fix broken links
...
This is done with a lua filter that rewrites links with regular
expressions.
References #480 .
2020-06-17 19:38:26 -04:00
Marko Dimjašević
3673bc8d26
Lambda: fix highlighting of bindings in the text
2020-06-07 22:38:34 +02:00
Marko Dimjašević
fed1bc2610
Properties: fix the rendering of a highlighted expression by removing a line break in the expression
2020-06-06 21:04:25 +02:00
Wen Kokke
8013d91afb
Pragmatic note on matching against decidable equality
2020-06-02 10:33:48 +01:00
Jeremy Siek
5bfc503eec
remove second premise from cong-rename
2020-05-20 09:05:06 -04:00
Liang-Ting Chen
33f0f64624
Fix cong-rename
...
M on the right hand side of ≡ should be M′
2020-05-20 16:12:54 +08:00
wadler
0a99b734ba
added line about imports for exercises to preface
2020-05-11 12:17:04 -03:00
Jeremy Siek
fcf981cfec
added explanation to exercise
2020-05-06 15:01:41 -04:00
Jeremy Siek
3d614523dc
fix mixup regarding former/later and description of import
2020-05-03 15:16:41 -04:00
Philip Wadler
77499be10c
Modified Peter's proposed text on argument order
2020-04-21 15:42:33 -03:00
Philip Wadler
8da824a96a
Add paragraph about order of arguments to x ≟ y
...
Thank you to Peter Thiemann for suggesting a paragraph on this subject.
2020-04-21 10:50:41 -03:00
Peter Thiemann
8b9fc489c3
pragmatic note on matching against decidable equality
2020-04-21 15:05:52 +02:00
Peter Thiemann
6ba26bbfc8
Agda 2.6.1 doesn't recognize it's terminating
2020-04-21 14:55:12 +02:00
wadler
6428b87def
added import to Qualifiers
2020-04-18 12:20:03 -03:00
wadler
c76da31328
merge
2020-04-17 12:16:18 -03:00
wadler
29157501d4
added proj_2 to imports in Qualifiers
2020-04-17 12:14:55 -03:00
Jeremy Siek
963fc985b0
moved exercise to come later
2020-04-10 13:55:52 -04:00
Jeremy Siek
09a91451b2
fix links
2020-04-09 09:27:24 -04:00
Jeremy Siek
433587bc61
more edits
2020-04-09 09:18:30 -04:00
Jeremy Siek
2afe5706a1
some edits
2020-04-09 09:15:25 -04:00
Jeremy Siek
2dc431121e
simplified D^c
2020-04-07 08:19:03 -04:00
Jeremy Siek
3ab180ad8d
tweak
2020-04-01 09:30:52 -04:00
Jeremy Siek
d1f628ceae
changed the denot-church exercise
2020-03-31 16:07:45 -04:00
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
850de4b860
fix typo
2020-03-30 15:57:23 -04: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
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
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
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
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
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
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
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
29dc9321d8
Minor clarifications on exercises in Naturals and Induction.
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
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
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
Marko Dimjašević
338b959f95
Properties: rename a proof for z ≢ x
2020-01-06 22:46:44 +01: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
Marko Dimjašević
ed97783252
Lambda: fix indentation for correct rendering
2019-12-29 22:37:49 +01: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
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
Wen Kokke
7680c90400
Merge pull request #432 from pedrominicz/dev
...
Fix: order of parameter in `split` function.
2019-11-08 12:21:21 +00:00
wadler
cbfd7d3be9
Merge branch 'dev' of github.com:plfa/plfa.github.io into dev
2019-11-06 11:29:54 +00:00
Philip Wadler
56124b56d7
Merge pull request #433 from omelkonian/asg4-imports
...
Consistent import of DB
2019-11-05 10:33:18 +00:00
Qais Patankar
617fe2a0ee
Fix missing backtick in Lambda
2019-11-02 14:27:58 +00:00
wadler
57a380f402
TSPL survey
2019-10-31 17:24:54 +00:00
Orestis Melkonian
eb3a727606
Consistent import of DB
...
* Re-export test examples from Chapter DeBruijn in Chapter More.
* In Chapter Inference, as well as Assignment 4, import the
instrinsically-typed λ-calculus as follows:
`import plfa.part2.More as DB`
2019-10-28 17:20:44 +00:00
wadler
9f0ae6e4b6
fixed exercise in List
2019-10-28 15:19:47 +00:00
wadler
749e6a9e57
renamed exercises
2019-10-28 12:00:38 +00:00
wadler
6f1933c141
minor fix to Inference
2019-10-28 11:14:22 +00:00
Pedro Minicz
edd3e83581
Improve explanation of split exercise.
2019-10-26 15:45:15 -03:00
Pedro Minicz
1f5fe587d9
Fix: order of parameter in split function.
...
The `merge` relation can be illustrated as follow:
merge xs ys zs ≡ xs + ys = zs
This shows a key point: every element of `xs` is contained in `zs`.
The original definition of `split` makes no sense under this revelation.
split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (xs : List A)
→ ∃[ ys ] ∃[ zs ] ( merge xs ys zs × All P ys × All (¬_ ∘ P) zs )
`zs` will contain all elements of `xs` (the input!) and we also have that `All (¬_ ∘ P) zs`. This function signature cannot be inhabited, as it would imply that for any `P : A → Set` and any `x : A` we have `¬(P x)`.
2019-10-26 15:25:03 -03:00
Pedro Minicz
0e1c5d34ea
Fix: make capitalization consistent.
2019-10-26 14:56:56 -03:00
Philip Wadler
eb03578439
Merge pull request #430 from citrusmunch/patch-2
...
consistent variable name typo
2019-10-26 10:44:51 +01:00
wadler
8656f2e7af
merge
2019-10-25 11:14:51 +01:00
wadler
a5960b6547
revised exercise More
2019-10-25 11:14:02 +01:00
citrusmunch
8d40127af0
consistent variable name typo
2019-10-24 21:30:59 -04:00
wadler
59796a6214
Update courses
2019-10-23 11:07:07 +01:00
Philip Wadler
9b2edd3f55
Merge pull request #385 from kenichi-asai/inference
...
Inference: a variable -> an abstraction
2019-10-21 16:13:09 +01:00
Pedro Minicz
1615048a31
Fix: missing close backquote on inline code.
2019-10-21 11:41:11 -03:00
Vi Po
23ab17728d
Fix Bit format
2019-10-20 22:25:39 +03:00
Philip Wadler
22edd31564
further tweaks to List
2019-10-14 19:11:14 +01:00
Philip Wadler
d13da5e92c
fixed merge on Lists
2019-10-14 15:54:59 +01:00
Philip Wadler
3494b05d56
Updating Lists
2019-10-14 15:52:19 +01:00
wadler
8c893ca669
Assignment 3
2019-10-14 12:02:08 +01:00
wadler
d8a42e68f9
added an example to beginning of Quantification
2019-10-07 10:59:15 +01:00
Wen Kokke
29d37040c2
Merge pull request #417 from momirza/patch-6
...
Remove redundant word
2019-09-30 13:33:33 +01:00
Wen Kokke
7a3ba37659
Merge pull request #418 from AD1024/dev
...
[ fix ] inline code block
2019-09-30 13:33:00 +01:00
wadler
55ecfb595b
Added Assignment2
2019-09-30 12:24:25 +01:00
AD1024
4d919d75e5
[ fix ] inline code block
2019-09-30 01:13:14 -07:00
Mo Mirza
eaa05fb1db
Remove redundant word
2019-09-29 02:01:42 +01:00
Wen Kokke
a79cd54db3
Merge pull request #415 from momirza/patch-4
...
Fix typo
2019-09-28 11:56:57 +01:00
Mo Mirza
739c9b4619
Remove “the”
2019-09-28 11:55:47 +01:00
Mo Mirza
2621c92824
Fix typo
2019-09-28 11:47:47 +01:00
AD1024
4991b56974
[ implement ] issue #412
2019-09-23 18:34:24 -07:00
wadler
8f77a13551
Revising Bin
2019-09-19 21:11:36 +01:00
Philip Wadler
f0af93fca8
Merge pull request #406 from plfa/string-compare
...
[WIP] Restructure Lambda now that String equality computes
2019-09-19 18:53:09 +01:00
Wen Kokke
4ccfa24b60
Moved explanation to Lambda#primed
2019-09-18 16:20:55 +01:00
Wen Kokke
ff882eccf6
Revert "Moved explanation to DeBruijn#lookup"
...
This reverts commit dba3a4ae84
2019-09-18 16:20:03 +01:00
Wen Kokke
c0086ca017
Revert "Removed ticked syntax exercise."
...
This reverts commit 598747b8e9
2019-09-18 16:13:22 +01:00
Reza Gharibi
4e3a2734dd
Removed an unnecessary import
2019-09-17 15:48:10 +02:00
Mo Mirza
1d44a3906a
Consistent formatting
2019-09-17 15:44:03 +02:00
Wen Kokke
dba3a4ae84
Moved explanation to DeBruijn#lookup
2019-09-17 15:34:18 +02:00
Wen Kokke
598747b8e9
Removed ticked syntax exercise.
2019-09-17 15:29:29 +02:00
Wen Kokke
eb3fac95b5
Removed 'assert inequality'; removed text explaining postulating impossible.
2019-09-17 15:11:13 +02:00
wadler
1b3b6f7cf1
minor fixes to assignments
2019-09-15 17:36:16 +01:00
Mo Mirza
5ae3b56ccc
Fix typo: argument to arguments
2019-09-11 00:32:52 +01:00
wadler
4841f3d879
added 'de Philip' to dedication
2019-09-05 17:37:39 +02:00
wadler
b0746f9e17
updated dedication
2019-09-05 16:35:17 +02:00
wadler
0de4fad2c0
updated dedication
2019-09-05 13:50:11 +02:00
Philip Wadler
68a128e819
Merge pull request #395 from h4iku/fix-name-typo
...
Fixed module naming typos
2019-09-04 12:56:00 +01:00
Wen Kokke
56189e2d87
Revert "Remove tick from constructors"
2019-09-03 17:19:14 +01:00
Philip Wadler
50f93f1e67
Merge pull request #394 from plfa/detick
...
Remove tick from constructors
2019-09-03 13:46:23 +01:00
Reza Gharibi
3a98d1dbae
Fixed module naming typos
2019-09-02 23:25:33 +04:30
wadler
07894d0d79
Remove tick from constructors
2019-09-02 19:15:50 +01:00
Reza Gharibi
0cb6b989d5
Changed the description of practice exercises
2019-09-01 03:00:42 +04:30
Reza Gharibi
63fcbbe25e
Changed missed inherent occurrences to intrinsic
2019-08-31 22:35:41 +01:00
wadler
f68782dccb
Change inherent to intrinsic
2019-08-31 20:04:12 +01:00
Turab Jafri
bb5ff4cd64
part1/Relations: Add _*_ import
...
For convenience, readers shouldn't worry about importing
functions that are required for exercises
2019-08-25 23:46:15 -04:00
Turab Jafri
aaf5b914b0
part1/Relations: Fix Typo
...
"form `m ≤ n`" -> "from `m ≤ n`"
2019-08-25 22:09:08 -04:00
Kenichi Asai
251d9bf751
Inference: a variable -> an abstraction
2019-08-23 09:25:24 +09:00
Jeremy Siek
69da80df93
agda style
2019-08-20 15:37:15 -04:00
Jeremy Siek
b88cd2478b
failed attempt to use std lib reasoning
2019-08-20 15:31:52 -04:00
