Expand description
Checks whether one type’s representation can be reinterpreted as another.
The analysis converts compiler layouts into trees of bytes, references, and
definition markers. It prunes destination paths that may carry safety invariants unless
safety is assumed, then converts the trees into deterministic finite automata.
Comparing the automata produces an Answer; reference transitions can leave
Conditions for the trait solver to discharge.
Modules§
Structs§
- Assume
- Proof obligations supplied by the caller rather than checked by the analysis.
- Transmute
Type Env