this repo includes some of the practice exercises from PLFA:
plfa.part1.Peano: associativity and distributivity proofs of + and * over +
plfa.part1.Relations: ≤ properties, trichotomy, even/odd proofs, bitstrings
plfa.part1.Relationsbinary: exercises (marked stretch) about bitstrings
plfa.part1.Negation: <-irreflexive, trichotomy with ≡/<, ⊎-dual-×
plfa.part1.Quantifiers: ∀-distrib-×, (∃[ x ] (x + y ≡ z)) ⇔ (y ≤ z), ∃-distrib-⊎
plfa.part1.Decidable: a few exercises, mostly copypasted definitions
plfa.part1.Lists: reverse-distrib-++, sum-downFrom, Any-++-⇔, All-++-≃
plfa.part2.Lambda: _[_:=_]′, mul, ⊢mul
plfa.part2.Properties: ⊢mul, automatic normalization of terms in ⊢mul-eval
but also just some exploratory agda "sketches" in sandbox/