Module expr

Modules

pretty 🔒

Macros

impl_ops 🔒

Structs

AliasReft

BoundReft

ESpan

EVid

Existential variable id

EarlyReftParam

Expr

FieldBind

KVar

In theory a kvar is just an unknown predicate that can use some variables in scope. In practice, fixpoint makes a difference between the first and the rest of the arguments, the first one being the kvar’s self argument. Fixpoint will only instantiate qualifiers that use the self argument. Flux generalizes the self argument to be a list. We call the rest of the arguments the scope.

KVid

Lambda

A lambda abstraction with an elaborated output sort. We need the output sort of lambdas for encoding into fixpoint

Name

Path

Real

Enums

AggregateKind

BinOp

Constant

Ctor

ExprKind

FieldProj

HoleKind

The position where a hole appears. This determines how it will be inferred. This is related to, but not the same as, an InferMode.

Loc

UnOp

Var