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
