Module analyse

An infrastructure to mechanically analyse proof trees.

It is unavoidable that this representation is somewhat lossy as it should hide quite a few semantically relevant things, e.g. canonicalization and the order of nested goals.

@lcnr: However, a lot of the weirdness here is not strictly necessary and could be improved in the future. This is mostly good enough for coherence right now and was annoying to implement, so I am leaving it as is until we start using it for something else.

Structs

• InspectCandidate
• InspectConfig
• InspectGoal
• NormalizesToTermHack 🔒
  The expected term of a NormalizesTo goal gets replaced with an unconstrained inference variable when computing NormalizesTo goals and we return the nested goals to the caller, who also equates the actual term with the expected.

Traits

• ProofTreeInferCtxtExt
• ProofTreeVisitor
  The public API to interact with proof trees.