wadler
af45cdcfdb
Merge branch 'dev' of github.com:plfa/plfa.github.io into dev
2021-08-29 18:37:14 +01:00
Lorenzo Lipparini
d2c14f40e1
Fix coding style inconsistencies in part1/Quantifiers
2021-08-29 15:26:34 +02:00
wadler
6ea7439507
Merge branch 'dev' of github.com:plfa/plfa.github.io into dev
2021-08-29 10:33:10 +01:00
Philip Wadler
3e03d1ee03
Update Lists.lagda.md
2021-08-29 10:29:46 +01:00
wadler
27006a8181
fixed Assignment4
2021-08-28 18:28:04 +01:00
wadler
ba41d279f1
small changes: Subtyping, Inference, Assignment 4, Exam
2021-08-28 18:25:22 +01:00
Wen Kokke
a5e1f77d22
Changed header anchors. Commited WIP fix for #577 .
2021-08-25 11:53:30 +01:00
Wen Kokke
07d082c9db
Fixed syntax for assigning anchors.
2021-08-25 00:17:03 +01:00
Wen Kokke
e8df980d4b
Fixed PDF generate to use toc.metadata.
2021-08-24 15:00:50 +01:00
Wen Kokke
2987995c7a
WIP rewrite of book rendering.
2021-08-24 01:01:23 +01:00
Wen Kokke
d14b04ebf2
Fixed PDF generation.
2021-08-23 18:34:35 +01:00
Wen Kokke
7345c36d80
Fixed binding issues with existential syntax.
2021-08-23 11:57:30 +01:00
wadler
a162bcee5e
Merge branch 'dev' of github.com:plfa/plfa.github.io into dev
2021-08-10 17:51:19 +01:00
wadler
effcfb1e3e
fix typo in Confluence
2021-08-10 17:51:05 +01:00
Jeremy Siek
f7bc29d6f0
added accent
2021-07-29 10:46:23 -04:00
Jeremy Siek
67cbc3c837
added course in Torino
2021-07-29 10:45:30 -04:00
Wen Kokke
9691c05909
Fixed Agda errors; fixed css errors which resulted in the incorrect font being used.
2021-07-14 16:50:36 +01:00
Altaria
65536c8525
changed codeblocks comments to displays
2021-07-02 14:28:16 +01:00
wadler
00a04e43d1
small fix to Connectives
2021-06-26 15:43:48 +01:00
Altaria
dd370cd225
fix indentation on 736 to fix partial codeblocks
2021-06-25 16:14:28 +01:00
Altaria
0f8be19802
fixed indentation for proper code display
2021-06-25 11:22:18 +01:00
Altaria
724d8eb487
added new symbols in part2 and 3
2021-06-23 15:25:45 +01:00
Alexander Skiba
88763966a7
Fix typos and add a missing Unicode symbol
2021-03-10 03:24:51 +07:00
Andrés Sicard-Ramírez
bfe3060196
Fixed typos in the grammar for inherited terms.
2021-02-10 10:13:07 -05:00
wadler
3da42bdf23
revised hint for dagger exercise in bisimulation
2021-01-23 12:19:03 +00:00
wadler
946ac05513
Added mention of answer repository to preface and acknowledgements
2021-01-20 11:41:19 +00:00
Harrison Grodin
1174f18ff7
Fix typo
2020-12-25 21:21:12 -05:00
Philip Wadler
6503d1f076
Update preface.md
...
In response to #549 raised by Shreck Ye.
2020-12-22 18:31:35 +00:00
Cristóvão Gomes Ferreira (Melo Gibson)
40b63478ba
547 - Proving trans using ≡-Reasoning is circular
2020-12-03 20:19:16 +00:00
Marko Dimjašević
7c69576733
Bisimulation: fixes a verb form
2020-11-05 06:09:44 +01:00
Wen Kokke
396124156b
Fixed link error.
2020-10-26 17:41:12 +01:00
Wen Kokke
9b5ac3e7a8
Add section on citations to HOWTO.
2020-10-26 17:40:16 +01:00
Wen Kokke
2c4bf84365
Added support for citations.
2020-10-26 17:05:04 +01:00
Wen Kokke
d4821c9022
Fixed acknowledgements.
2020-10-24 17:14:15 +02:00
Marko Dimjašević
95b39edde5
More: align the names of parameters to #_ to those in Chapter DeBruijn ( #543 )
2020-10-24 17:14:05 +02:00
Marko Dimjašević
a9ecf866c2
More: fixes the syntax of substitution in a wrong translation of case× ( #532 )
...
* More: fixes the syntax of substitution in a wrong translation of case×
* More: fixes the names of projection functions in an intentionally wrong translation
2020-10-24 17:04:30 +02:00
Marko Dimjašević
753029e3ad
More: fixes the projection function used in the informal definition of from×⊤ ( #533 )
2020-10-24 17:03:53 +02:00
Marko Dimjašević
c70e990c29
More: aligns the formalisation of de Bruijn indices with that in the previous chapter ( #534 )
2020-10-24 17:02:29 +02:00
0xd34df00d
a38bdbac8c
Fix a tiny rendering bug due to a \n in inline code ( #536 )
2020-10-24 17:01:56 +02:00
Marko Dimjašević
0aff7d8b2d
More: improves readability of signatures for ext and rename ( #537 )
2020-10-24 17:01:30 +02:00
Marko Dimjašević
2db6d7754f
Make Γ and A parameters instead of indices to the _—↠_ relation ( #539 )
2020-10-24 17:01:09 +02:00
Marko Dimjašević
f0ca07c371
More: makes A a parameter to the Steps data type ( #541 )
2020-10-24 17:00:47 +02:00
Marko Dimjašević
ecec10e840
DeBruijn: refresh a function description given its new implementation ( #542 )
2020-10-24 17:00:27 +02:00
Marko Dimjašević
5326f16a8b
De Bruijn: fixes alignment of arguments to #_ ( #535 )
2020-10-24 16:59:43 +02:00
Wen Kokke
0441f97d8c
Fixed citation page. Added announcement. Removed old build files.
2020-10-23 14:51:10 +02:00
Wen Kokke
3d4c9f7a1d
Fixed rendering errors.
2020-10-23 11:21:02 +02:00
Wen Kokke
2c82ce21da
Switch to Hakyll as the build system for PLFA ( #540 )
2020-10-23 08:45:49 +02:00
Philip Wadler
ea8bee4461
Merge pull request #514 from mdimjasevic/debruijn-wo-impossible
...
DeBruijn: introduce a version of #_ that depends on no postulate
2020-10-17 12:47:47 +01:00
Marko Dimjašević
ea1b9c2150
More: fixes an informal definition of swap×
2020-10-14 18:12:16 +02:00
Philip Wadler
20516d9e8e
Merge pull request #525 from bollu/emacs-keybinds-mnemonics
...
Add mnemonics when keys are first introduced
2020-10-13 12:49:50 +01:00
