Modules§
- pretty 🔒
Macros§
- impl_
ops 🔒
Structs§
- Alias
Reft - Bound
Reft - ESpan
- EVid
- Existential variable id
- Early
Reft Param - Expr
- Field
Bind - 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§
- Aggregate
Kind - BinOp
- Constant
- Ctor
- Expr
Kind - Field
Proj - Hole
Kind - The position where a hole appears. This determines how it will be inferred. This is related
to, but not the same as, an
InferMode. - Internal
Func Kind - Primitive Properties
- Loc
- Spec
Func Kind - UnOp
- Var