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 distinguishes a list of leading arguments, the kvar’s self arguments, from the rest,
which we call the scope. Fixpoint only instantiates qualifiers whose first parameter is a self
argument, so a kvar without self arguments can only be solved to
trueorfalse. The number of self arguments is passed to fixpoint with the:selfannotation. - KVid
- Lambda
- A lambda abstraction with an elaborated output sort. We need the output sort of lambdas for encoding into fixpoint
- Name
- Path
- Pretty
Map - RawPtr
Field 🔒Data - Real
- WKVar
- A weak kvar is like a kvar with the exception that it infers the weakest condition necessary instead of the strongest condition. Due to the way we generate these kvars (on fn_sigs, rather than during constraint generation), they also in theory are global.
- WKVid
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
- Name
Provenance - Pretty
Var - Quant
Dom - RawPtr
Field - Spec
Func Kind - UnOp
- Var