Module typed

Structs

ElimCase

A lazy pattern match reified as a Rust type.

ElimProj

Pure

WeakHead

Weak head reduction type (equivalent to applying a reduction to the head variable, but this way we don’t have to implement variable lookup and it doesn’t serialize with variables).

Traits

SubContext

SynthTyped

Given a head expression (Self) and a target type (Type), attempt to synthesize a term that reduces head into the target type.

Typed

Type Aliases

ElimWeak