Search results

Simpler proof of Isomorphism.≲-antisym

Status: Open.

#1203 In plfa/plfa.github.io;

· peterthiemann opened on Jun 3, 2026

Build output has too many line breaks

Status: Open.

#1144 In plfa/plfa.github.io;

· blntk opened on Nov 6, 2025

eta equality should be motivated/explained

Status: Open.

#1099 In plfa/plfa.github.io;

· fangyi-zhou opened on Feb 12, 2025

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

Status: Open.

#1019 In plfa/plfa.github.io;

· nrnrnr opened on Jul 24, 2024

Slow workflow for contributors

Status: Open.

#1018 In plfa/plfa.github.io;

· nrnrnr opened on Jul 23, 2024

Something seems to be missing in chapter Naturals

Status: Open.

#1016 In plfa/plfa.github.io;

· cmsmcq opened on Jul 22, 2024

Type suggested in exercise Bin-isomorphism does not compile.

Status: Open.

#1003 In plfa/plfa.github.io;

· nrnrnr opened on Jun 3, 2024

Repository is too large

Status: Open.

#993 In plfa/plfa.github.io;

· wenkokke opened on May 4, 2024

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

Status: Open.

#992 In plfa/plfa.github.io;

· adql opened on May 4, 2024

a:visited in code blocks messes up highlighting

Status: Open.

#989 In plfa/plfa.github.io;

· adql opened on May 2, 2024

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

Status: Open.

#877 In plfa/plfa.github.io;

· michaelpj opened on May 31, 2023

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

Status: Open.

#872 In plfa/plfa.github.io;

· michaelpj opened on May 29, 2023