Expand description
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§
Traits§
- Infer
Ctxt Proof Tree Ext - Proof
Tree Visitor - The public API to interact with proof trees.