Issues

• CI on a fresh fork failing (HTMLProofer)

  plfa/plfa.github.io#1229 · Filter by author JacquesCarette opened on Sep 9, 2026

• Simpler proof of Isomorphism.≲-antisym

  plfa/plfa.github.io#1203 · Filter by author peterthiemann opened on Jun 3, 2026
  2

• Build output has too many line breaks

  plfa/plfa.github.io#1144 · Filter by author blntk opened on Nov 6, 2025
  5

• eta equality should be motivated/explained

  plfa/plfa.github.io#1099 · Filter by author fangyi-zhou opened on Feb 12, 2025
  4

• The Confluence chapter uses Subst without definition, comment, or forward reference

  plfa/plfa.github.io#1019 · Filter by author nrnrnr opened on Jul 24, 2024
  

• Slow workflow for contributors

  plfa/plfa.github.io#1018 · Filter by author nrnrnr opened on Jul 23, 2024
  10

• Something seems to be missing in chapter Naturals

  plfa/plfa.github.io#1016 · Filter by author cmsmcq opened on Jul 22, 2024
  1

• Type suggested in exercise Bin-isomorphism does not compile.

  plfa/plfa.github.io#1003 · Filter by author nrnrnr opened on Jun 3, 2024
  3

• Repository is too large

  plfa/plfa.github.io#993 · Filter by author wenkokke opened on May 4, 2024
  1

• Exercise ⊎-dual-× (part1.Negation): add a note about imports

  plfa/plfa.github.io#992 · Filter by author adql opened on May 4, 2024
  3

• a:visited in code blocks messes up highlighting

  plfa/plfa.github.io#989 · Filter by author adql opened on May 2, 2024
  7

• The definition of sigma could draw attention to the use of forall

  plfa/plfa.github.io#877 · Filter by author michaelpj opened on May 31, 2023
  3

• The 'Bin' stretch exercise in 'Induction' requires re-defining code from previous exercise

  plfa/plfa.github.io#872 · Filter by author michaelpj opened on May 29, 2023
  3

• Substitution.commute-subst-rename is weird

  plfa/plfa.github.io#858 · Filter by author crisoagf opened on Apr 19, 2023
  1

• Unclear which nats.agda file is being referred to in "Getting Started"

  plfa/plfa.github.io#854 · Filter by author bzm3r opened on Mar 29, 2023

• Investigate a denotation type that is inherently downward closed

  agdaenhancementtext
  plfa/plfa.github.io#704 · Filter by author jsiek opened on Jun 22, 2022
  

• Write instructions for development using branches and PRs

  documentationenhancement
  plfa/plfa.github.io#689 · Filter by author wenkokke opened on Jun 15, 2022

• Publish build and test reports

  accessibilitydocumentationenhancement
  plfa/plfa.github.io#685 · Filter by author wenkokke opened on Jun 15, 2022

• Compile course PDFs as part of build

  enhancementhelp wantedlow-hanging-fruit
  plfa/plfa.github.io#684 · Filter by author wenkokke opened on Jun 15, 2022

• Add descriptions to anchor links

  accessibilityhelp wantedlow-hanging-fruit
  plfa/plfa.github.io#683 · Filter by author wenkokke opened on Jun 15, 2022

• Resolve inconsistent use of headers

  accessibilitybugmarkup
  plfa/plfa.github.io#680 · Filter by author wenkokke opened on Jun 9, 2022

• Integrate DAISY Ace into CI

  accessibilitybuildenhancementepub
  plfa/plfa.github.io#675 · Filter by author wenkokke opened on Jun 9, 2022

• Styling issues for Agda code in EPUB

  accessibilityepubhelp wantedstyle
  plfa/plfa.github.io#673 · Filter by author wenkokke opened on Jun 9, 2022

• Build PDF version

  buildenhancementhelp wantedpdf
  plfa/plfa.github.io#672 · Filter by author wenkokke opened on Jun 9, 2022
  9

• Create test page for TeX math

  enhancement
  plfa/plfa.github.io#669 · Filter by author wenkokke opened on Jun 9, 2022