Wen Kokke
|
eb6e9d93c5
|
Fix small error
|
2020-05-22 20:46:40 +01:00 |
|
Wen Kokke
|
5ae6438e8f
|
Restructured Getting Started.
|
2020-05-22 20:45:35 +01:00 |
|
Wen Kokke
|
6700cf597d
|
Rewrote Getting Started to provide instructions for installing a specific version of Agda.
|
2020-05-22 18:21:25 +01:00 |
|
Wen Kokke
|
8d59de6394
|
Added rewrite of Inference by Prabhakar
|
2020-05-22 15:50:50 +01:00 |
|
Wen Kokke
|
7eea42d370
|
Minor changes in highlight script.
|
2020-05-22 15:46:54 +01:00 |
|
Jeremy Siek
|
5bfc503eec
|
remove second premise from cong-rename
|
2020-05-20 09:05:06 -04:00 |
|
Jeremy G. Siek
|
bfff5d01cb
|
Merge pull request #474 from L-TChen/patch-1
Fix cong-rename
|
2020-05-20 09:03:04 -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 |
|
wadler
|
6a3fec78b6
|
updates to index page
|
2020-04-30 15:23:40 -03:00 |
|
wadler
|
f2cb91fc30
|
added Levy suggestion to extra
|
2020-04-30 08:36:48 -03: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
|
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 |
|