Module red 

“Chains” are a canonicalized form of types/permissions. They can only be produced after inference is complete as they require enumerating the bounds of inference variables. They are used in borrow checking and for producing the final version of each inference variable.

Modules

lattice

sub

Structs

Live

RedChain 🔒

RedPerm 🔒

A “lien chain” is a list of permissions by which some data may have been reached. An empty lien chain corresponds to owned data (my, in surface Dada syntax). A lien chain like ref[p] mut[q] would correspond to data referencing a variable p which in turn had data mutable from q (which in turn owned the data).

Enums

RedLink 🔒

RedTy

A “red(uced) type”– captures just the type layout part of a SymGenericTerm.