Structs

Functions

create 🔒

Type Definitions

As part of computing the free region relations, we also have to normalize the input-output types, which we then need later. So we return those. This vector consists of first the input types and then the output type as the last element.

Each RBP ('a, GK) indicates that GK: 'a can be assumed to be true. These encode relationships like T: 'a that are added via implicit bounds.