Commit graph

  • e2916d7642
    Update Naturals.lagda.md Matthias Gabriel 2020-02-13 12:49:51 +0100
  • 6af4de708a Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Jeremy Siek (via Travis CI) 2020-02-11 21:02:58 +0000
  • f3fa4feb95 simpler hint for Bin-isomorphism Jeremy Siek 2020-02-11 15:50:30 -0500
  • 2a55bde7ef Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Wen Kokke (via Travis CI) 2020-02-10 14:38:49 +0000
  • 50508c9dd7 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Wen Kokke (via Travis CI) 2020-02-08 14:45:46 +0000
  • e2746aaaba Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Wen Kokke (via Travis CI) 2020-02-08 14:39:30 +0000
  • 1c06cd319d
    Merge pull request #463 from plfa/zachrbrown-dev Wen Kokke 2020-02-08 14:32:04 +0000
  • 84556ab62e Minor fix Wen Kokke 2020-02-08 14:30:29 +0000
  • aaaabb1a20
    Merge pull request #462 from fangyi-zhou/anchors Wen Kokke 2020-02-08 14:27:39 +0000
  • f4776a9df4
    Use anchorjs for generating anchors Fangyi Zhou 2020-02-07 23:31:20 +0000
  • 310ab57692 Address PR feedback — remove additional agda specifics Zachary Brown 2020-02-06 17:04:02 -0800
  • d361456333 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Jeremy Siek (via Travis CI) 2020-02-03 14:38:40 +0000
  • a41306ce2d Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Jeremy Siek (via Travis CI) 2020-02-01 19:48:26 +0000
  • 7c1d4d7903 added to the hint Jeremy Siek 2020-02-01 14:36:58 -0500
  • 25fbc53ecb Add note about agda pragma placement Zachary Brown 2020-01-29 15:56:50 -0800
  • 72a8937098 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-27 21:41:36 +0000
  • fae067dc53 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Jeremy Siek (via Travis CI) 2020-01-27 21:30:05 +0000
  • c50f5713bc
    Merge pull request #458 from mdimjasevic/denot-untyped-to Philip Wadler 2020-01-27 15:27:38 -0600
  • eae2f16659 fix a typo Jeremy Siek 2020-01-27 16:18:00 -0500
  • 0c58f450a3 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-27 21:11:32 +0000
  • 83b8e6da00
    Merge pull request #452 from mdimjasevic/prop-preserve-beta Philip Wadler 2020-01-27 14:59:33 -0600
  • 8aff938f71
    Denotational: remove a double 'to' Marko Dimjašević 2020-01-27 21:42:17 +0100
  • 7e5e38fe06 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-27 20:21:48 +0000
  • d7143136ef
    Merge pull request #453 from mdimjasevic/prop-vis-align Philip Wadler 2020-01-27 14:09:47 -0600
  • f401b26aba Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-27 16:53:07 +0000
  • 2a7bf78b19
    Merge pull request #456 from mdimjasevic/prop-two-plurals Philip Wadler 2020-01-27 10:41:35 -0600
  • 5e1c2cd283 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-27 14:38:02 +0000
  • 28c5258671 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-26 19:35:08 +0000
  • 0e5a71ec1e
    Merge pull request #457 from mdimjasevic/prop-well-typed-2 Philip Wadler 2020-01-26 13:23:55 -0600
  • 557a088c78
    Properties: fix 'well-typed' according to issue #318 Marko Dimjašević 2020-01-26 10:26:36 +0100
  • 6516a5d7ba
    Properties: fix a double plural mistake Marko Dimjašević 2020-01-25 11:20:46 +0100
  • 643ff85cd0
    Properties: visual alignment of pattern matches for M —→ N in the proof of preserve Marko Dimjašević 2020-01-24 14:59:10 +0100
  • 495123979c
    Properties: fixes an informal rule in the text for β-ƛ by using a reduction relation instead of the typing judgment Marko Dimjašević 2020-01-22 22:28:05 +0100
  • 05550802df Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Wen Kokke (via Travis CI) 2020-01-21 20:24:15 +0000
  • 00bd32e7ac Fixed bug in link Wen Kokke 2020-01-21 20:14:09 +0000
  • 4ad9a0da8a Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Wen Kokke (via Travis CI) 2020-01-21 17:18:39 +0000
  • d70f12a8aa
    Merge pull request #438 from qaisjp/patch-1 Wen Kokke 2020-01-21 17:05:14 +0000
  • 29dc9321d8 Minor clarifications on exercises in Naturals and Induction. Wen Kokke 2020-01-21 17:03:56 +0000
  • 0003b0465f Fix #451 - mention mailing lists Wen Kokke 2020-01-21 17:03:22 +0000
  • 766ca6ccce Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Jeremy Siek (via Travis CI) 2020-01-20 14:40:23 +0000
  • 0496f9bb62 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Jeremy Siek (via Travis CI) 2020-01-19 18:43:48 +0000
  • f6606a8ee6 added hint to exercise forall-x Jeremy Siek 2020-01-19 13:32:27 -0500
  • 43a70e1fef Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Jeremy Siek (via Travis CI) 2020-01-19 02:50:03 +0000
  • ea42753758 added hints to Bin-isomorphism exercise Jeremy Siek 2020-01-18 21:38:42 -0500
  • 2563b25f03 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master wadler (via Travis CI) 2020-01-14 13:36:42 +0000
  • 435bf28a9e merge wadler 2020-01-14 10:26:02 -0300
  • d770366fb4 added SF meetup to home page wadler 2020-01-14 10:24:39 -0300
  • 934477ddfc Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-13 16:05:04 +0000
  • d26fd33118
    Merge pull request #450 from mdimjasevic/prop-abs-ind Philip Wadler 2020-01-13 12:52:49 -0300
  • 4ba73c4065 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-13 14:37:32 +0000
  • 776f10940d
    Properties: fix the inductive hypothesis for lambda abstraction in the description of the proof of subst Marko Dimjašević 2020-01-13 10:45:46 +0100
  • fe7a3565d0 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-10 14:54:28 +0000
  • d3ebc6cd94 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-10 14:50:32 +0000
  • a49205abd3
    Remove redundant text Philip Wadler 2020-01-10 11:41:20 -0300
  • 170496699b
    Merge pull request #449 from ywata/emacs-unicode Philip Wadler 2020-01-10 11:38:56 -0300
  • 896b2b528a
    Further edits Philip Wadler 2020-01-10 11:38:28 -0300
  • 6b8e61c1e7 Mention emacs commands in Unicode section. YASUHIKO WATANABE 2020-01-10 23:19:33 +0900
  • eb68d083a7 Mention some emacs commands. YASUHIKO WATANABE 2020-01-10 23:18:41 +0900
  • 58e8a5ac12 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master wadler (via Travis CI) 2020-01-10 14:15:05 +0000
  • 1fd075440f fixed error in Lists wadler 2020-01-10 11:02:28 -0300
  • 77a87549f6 Merge branch 'dev' of github.com:plfa/plfa.github.io into dev wadler 2020-01-10 10:58:58 -0300
  • fc5f645ecb added link to Nextjournal wadler 2020-01-10 10:58:41 -0300
  • e6ba05ee89 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Jeremy Siek (via Travis CI) 2020-01-08 19:34:05 +0000
  • 95fa648a23 added link to course at Indiana Jeremy Siek 2020-01-08 14:19:30 -0500
  • c87bb1a6d5 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2020-01-06 23:30:28 +0000
  • 981f7850cd
    Merge pull request #447 from mdimjasevic/prop-swap-prf-name Philip Wadler 2020-01-06 20:19:29 -0300
  • 338b959f95
    Properties: rename a proof for z ≢ x Marko Dimjašević 2020-01-06 22:46:44 +0100
  • 6842ac170b merge Philip Wadler 2020-01-05 22:36:53 +0000
  • 784f99a406 Small changes to send-marks Philip Wadler 2020-01-05 22:36:10 +0000
  • 4bcd2f4f0b Travis CI deployment is broken. Wen Kokke 2020-01-03 16:24:41 +0000
  • 733f1d9212 Fix #446 Wen Kokke 2020-01-03 15:56:50 +0000
  • 9f6e3125e7 Fixed #445 Wen Kokke 2020-01-03 15:24:02 +0000
  • 4d393171db
    Merge pull request #444 from mdimjasevic/lambda-typing-inj Philip Wadler 2020-01-03 08:54:13 -0300
  • 3a3539bb77 Lambda: fix the term in an example showing typing relation is not injective Marko Dimjašević 2020-01-03 08:50:22 +0100
  • 233bac8071
    Merge pull request #443 from mdimjasevic/lambda-indent-impossible Philip Wadler 2019-12-30 01:13:24 -0300
  • ed97783252 Lambda: fix indentation for correct rendering Marko Dimjašević 2019-12-29 22:37:49 +0100
  • 5547b5251e
    Merge pull request #442 from mdimjasevic/lambda-suc-con Philip Wadler 2019-12-28 21:53:55 +0000
  • 35e66258cc Lambda: make the argument name consistent with the latter text Marko Dimjašević 2019-12-28 22:47:03 +0100
  • 461c574f8d Lambda: give the suc constructor is the text with an argument Marko Dimjašević 2019-12-28 22:40:02 +0100
  • a77284a415 added icfp tutorial wadler 2019-12-28 16:47:01 -0300
  • 98cb552b38 merge Philip Wadler 2019-12-09 12:44:24 +0000
  • a8eaea3e47 updated Exam to remove mock Philip Wadler 2019-12-09 12:43:59 +0000
  • 2d2b7c7fe9
    Merge pull request #441 from googleson78/infixr-sum Philip Wadler 2019-12-02 13:18:33 -0300
  • ef7f95b1db Make sum type right-associative Georgi Lyubenov 2019-12-02 09:49:49 +0200
  • 32a626789b Fix #227 Wen Kokke 2019-11-29 13:16:07 +0000
  • 88ce889159 merge Philip Wadler 2019-11-19 12:52:32 +0000
  • fd35c7b992 instructions for essay Philip Wadler 2019-11-19 12:51:59 +0000
  • 9cc7a9b29b Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master wadler (via Travis CI) 2019-11-15 11:15:49 +0000
  • f4593c8433 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2019-11-15 11:09:28 +0000
  • 26ead770bf added exam instructions wadler 2019-11-15 11:00:44 +0000
  • 345d422605 added mocks Philip Wadler 2019-11-15 10:55:08 +0000
  • ddb9b75c16
    Fix white-space breaking for multiline code blocks Qais Patankar 2019-11-13 14:13:58 +0000
  • 5c504b063a Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Philip Wadler (via Travis CI) 2019-11-13 10:06:28 +0000
  • b885666c03 added recursive types Philip Wadler 2019-11-13 09:54:27 +0000
  • 04a52de159
    Avoid line breaks in the middle of code Qais Patankar 2019-11-13 04:37:03 +0000
  • d189895063 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master Wen Kokke (via Travis CI) 2019-11-12 22:55:04 +0000
  • 2ee8a33a4f
    Merge pull request #437 from qaisjp/feature/page-break Wen Kokke 2019-11-12 22:43:10 +0000
  • 2139c9edd3 Deploy plfa/plfa.github.io to github.com/plfa/plfa.github.io.git:master wadler (via Travis CI) 2019-11-12 21:18:29 +0000
  • 38cd3659ca merge wadler 2019-11-12 21:05:11 +0000
  • 60090ed190 updated TSPL page wadler 2019-11-12 21:01:32 +0000