design question: what are good placeholders in proofs?

[jwaldmann]

If I want to give exercise questions of the kind "complete this (partial) proof", then I need to mark positions in a proof tree where students can fill in stuff.

(and I need to check that they did not change the tree in other places, but this issue is not about implementation, it is about design)

I think there are two kinds of "proof holes"

• single hole
  • a hole for an expression (it can be as simple as (by def foo) .=. <hole> - the student
    has to insert the result of the rewrite step)
  • a hole for a (sub)proof (any subtree of a ParseProof, etc.) (cyp has "by cheating" already?)
• "list hole" (where the AST requires a list of things, more items can be inserted)
  • list of equational rewrite steps
  • list of lemmas

What would be good (uniform) notation for that? Preferrable, notation that is understood by cyp,
so it does not crash, but gives a message "partial proof, need to fill hole(s) at ..." and continues processing in some meaningful way (if possible).

(Implemenation for Haskell Lückentexte: https://gitlab.imn.htwk-leipzig.de/autotool/all0/blob/master/collection/src/Haskell/Blueprint/Match.hs . I don't use "list holes" there, in fact, it was in the matching code, but I switched it off)