Module substitute 

Capture-avoiding substitution

Structs

Closing

A closing substitution is used to map free variables into bound variables when converting a type being built in a context to a closed(ish) type that is above that context.

Innerize

An innerize substitution is used to bring an outer type alias inwards through one context.

Opening

An opening substitution is used to map bound variables into free variables. Note that because of the differences in ordering for bound variable indices (inside out) and context variables (left to right, but variables are inserted in outside-in order), Bound(0) gets mapped to Free(0, base + n).

Shifted

A “shifted” version of a substitution, used internally to assure that substitution is capture-avoiding.

Enums

ClosingError

Closing can fail for a few reasons:

InnerizeError

Innerizing can fail because a type variable needs to be taken through an outer_boundary but cannot be resolved to a concrete type that can be copied.

Void

The empty (void) type

Traits

Shiftable

A substitution that can be converted into a Shifted substitution. All types other than Shifted itself should implement this with the obvious option of

Substitution

A substitution

Unvoidable

Things that you can call not_void on