Marko Dimjašević
8863ed75d1
De Bruijn: makes type A a parameter to the Steps data type ( #528 )
2020-10-12 12:05:46 +02:00
Oliver Tušla
63ab946579
fix link to Agda docs ( #529 )
2020-10-12 11:52:18 +02:00
Marko Dimjašević
adab54f36d
De Bruijn: Fix a verb form ( #527 )
2020-10-05 17:17:06 +02:00
Marko Dimjašević
a78889398d
De Bruijn: fix a line-break in the middle of a markup ( #526 )
2020-10-05 17:14:00 +02:00
Siddharth
242666d380
Mnemonics the first time keys are introduced
...
Add mnemonics for each of the key bindings which have a mnemonic. This makes it easier to learn the bindings.
2020-10-03 13:11:18 +05:30
Marko Dimjašević
f4a6f941a0
De Bruijn: Implements Wadler's feedback to PR #514
2020-10-02 14:18:37 +02:00
Marko Dimjašević
41d7e373ce
De Bruijn: changes the alignment of function arguments for consistency
2020-10-02 13:33:42 +02:00
Marko Dimjašević
a889fa0273
De Bruijn: implement feedback to PR #514 by Wadler and Kokke
2020-10-01 22:33:59 +02:00
Marko Dimjašević
ef3b3b00aa
Adds a missing closing parenthesis
2020-09-25 12:18:56 +02:00
Reza Gharibi
778d42371d
Fixed some typos ( #519 )
2020-09-25 10:40:46 +02:00
Marko Dimjašević
edcf159ea9
DeBruijn: update a figure in the golden section to reflect a change in representation
2020-09-22 07:51:29 +02:00
Reza Gharibi
33576e4345
Fixed some typos
2020-09-17 20:49:59 +04:30
Marko Dimjašević
318ff6f491
Polishes an updated alternative formalisation of variables via de Bruijn indices
2020-09-12 23:00:35 +02:00
Marko Dimjašević
375df5c3c5
DeBruijn: introduce a version of #_ that depends on no postulate
2020-09-11 23:26:34 +02:00
Marko Dimjašević
ebdd29865b
Fixes a verb plural error ( #512 )
2020-09-10 07:39:40 +02:00
Gagan Devagiri
018113ee02
Fix typos ( #508 )
2020-08-19 23:27:52 +02:00
Wen Kokke
f06137a621
Added fix-whitespace.yaml and fixed whitespace.
2020-08-19 21:54:32 +02:00
Matthew Healy
a591bf8616
Fix newline rendering in Quantifiers chapter ( #498 )
2020-08-19 19:44:36 +02:00
Gan Shen
b87defd53d
fix missing O ( #502 )
2020-08-18 09:52:46 +02:00
Dee Yeum
f31dae473e
Add documentation link to Agda pragmas
2020-08-05 16:23:19 +09:00
Matthew Healy
fd10b0d5a9
Fix newline rendering in Decidable chapter
2020-07-31 16:04:16 +02:00
Marko Dimjašević
6a2f296e32
Properties: introduce an implicit argument M for clarity in the type of M-named variables ( #454 )
2020-07-24 18:50:20 +01:00
purchan
4e40ef4ab3
part1/Decidable: Renaming proof ( #496 )
2020-07-24 18:48:25 +01:00
Liang-Ting Chen
4e287a06f1
[ re #473 ] Takahashi's complete development ( #493 )
2020-07-24 18:47:30 +01:00
Philip Wadler
dd32f8f6c6
Update Negation.lagda.md
...
At suggestion of Fredrik Nordvall Forsberg, replace "proof by contradiction" with "reductio ad absurdum".
2020-07-23 12:12:43 +01:00
Wen Kokke
0615638d66
Upgrade to Agda v2.6.1. ( #492 )
2020-07-19 19:43:20 +01:00
Wen Kokke
935362efc4
Fix #495 .
2020-07-19 13:56:36 +01:00
wadler
4423c37089
small fixes
2020-07-17 18:45:36 +01:00
Jeremy Siek
5095ca11c1
tweak
2020-07-17 10:08:38 -04:00
Jeremy Siek
b538aba98b
moving infix decls
2020-07-17 10:04:59 -04:00
Jeremy Siek
1052db99b3
more tweaks
2020-07-17 09:58:15 -04:00
Jeremy Siek
711cd4fff5
tweaks
2020-07-17 09:53:59 -04:00
Jeremy Siek
71e8f13fc3
spell check
2020-07-17 09:41:57 -04:00
Jeremy Siek
3398281a67
finished references
2020-07-17 09:30:06 -04:00
Jeremy Siek
03e710febf
finished preservation, so the first draft of Subtyping is complete
2020-07-16 22:19:36 -04:00
Jeremy Siek
1e14534a8d
progress :) finished Progress
2020-07-16 17:29:21 -04:00
Jeremy Siek
dbc9f0aac8
text through <:-trans
2020-07-16 16:06:51 -04:00
Jeremy Siek
a8682af3d4
text through <:-refl
2020-07-16 14:55:03 -04:00
Philip Wadler
b6b128c337
Merge pull request #494 from matthew-healy/even-odd-spacing
...
Align type definitions in even and odd example
2020-07-16 19:35:56 +01:00
Matthew Healy
2a620487f6
Align types in even and odd example
2020-07-16 18:31:16 +02:00
Jeremy Siek
f14ddf42ec
first draft of Subtyping, still needs some text
2020-07-15 17:06:42 -04:00
Wen Kokke
a79af92920
Minor changes.
2020-07-15 14:24:38 +01:00
Wen Kokke
2d5270a4e7
Updating citing
2020-07-14 19:54:00 +01:00
Wen Kokke
48dcc99152
Removed statistics page.
2020-07-14 18:12:21 +01:00
Wen Kokke
74d8781297
Fixed issue with EPUB.
2020-07-13 23:50:28 +01:00
Wen Kokke
11d8dff177
Replace use of impossible idiom with proof by reflection ( #409 )
...
* Added section on proof by reflection to Decidable.
* Define True in Decidable.
* Add exercise for defining False in Decidable.
* Rewrote text in Lambda to reflection new section on proof by reflection.
* Replace S constructor in Lambda with a version which checks the inequality implicitly.
* Define product and unit types as records in Connectives.
* Explain difference between data and records w.r.t. definitional equality in Connectives.
2020-07-13 23:01:14 +01:00
Wen Kokke
d3a7a60060
Merge pull request #489 from plfa/issue488
...
Fix #488
2020-07-13 22:56:27 +01:00
Wen Kokke
f04dbd2c65
Updated Lambda to specify determinism implies the diamond property and confluence, but the diamond property does not imply confluence by itself.e
2020-07-13 15:03:00 +01:00
wadler
697174cd47
merge
2020-07-08 11:50:27 +01:00
wadler
78da4246b6
improved intro to cong4
2020-07-08 11:50:04 +01:00
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
