  Cyp (Check Your Proofs) (Durner and Noschinski 2013; Traytel 2019) verifies
proofs about Haskell-like programs. We extended Cyp with a pattern matcher for
programs and proof terms, and a type checker.
  This allows to use Cyp for auto-grading exercises where the goal is to
complete programs and proofs that are partially given by the instructor, as
terms with holes. Since this allows holes in programs, type-checking becomes
essential. Before, Cyp assumed that the program was written by a type-correct
instructor, and therefore omitted type-checking of proofs. Cyp gracefully
handles incomplete student submissions. It accepts holes temporarily, and
checks complete subtrees fully.
  We present basic design decisions, make some remarks on implementation, and
include example exercises from a recent course that used Cyp as part of the
Leipzig Autotool auto-grading system.
