Module expr

Modules

• pretty 🔒

Macros

• impl_ops 🔒

Structs

• AliasReft
• BoundReft
• ESpan
• EarlyReftParam
• Expr
• 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
• 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