Modules§
- pretty 🔒
Structs§
- Cursor
- A cursor into the refinement tree. More specifically, a
Cursorrepresents a path from the root to some internal node in a refinement tree. - Marker
- A marker is a pointer to a node in the refinement tree that can be used to query information about that node or to move the cursor. A marker may become invalid if the underlying node is cleared.
- Node 🔒
- NodePtr 🔒
- Parents
Iter 🔒 - RcxBind 🔒
- Refine
Ctxt Trace - An explicit representation of a path in the
RefineTreeused for debugging/tracing/serialization ONLY. - Refine
Tree - A refinement tree tracks the “tree-like structure” of refinement variables and predicates generated during refinement type-checking. This tree can be encoded as a fixpoint constraint whose satisfiability implies the safety of a function.
- Scope
- A list of refinement variables and their sorts.
- Unpacker
- Weak
Node 🔒Ptr