Struct mm0b_parser::Type [−][src]
#[repr(C)]pub struct Type(_);
Expand description
An argument binder in a term/def or axiom/theorem.
- Bit 63 (the high bit of the high byte) is 1 if this is a bound variable.
- Bits 56-62 (the low 7 bits of the high byte) give the sort of the variable.
- Bits 0-55 (the low 7 bytes) are a bitset giving the set of bound variables earlier in the list that this variable is allowed to depend on.
Implementations
Get the u64 comprising a type
Make a new Type
of sort sort_num
Annotate a Type
with a sort.
Since types are often built incrementally, you may have built a “blank”
type that you knew was bound, but you’ll only know it’s sort later.
This is how you add the sort. If the Type
already had a sort,
it’s overwritten by sort_id
.
Does this type depend on the bth bound variable?
This is 0 indexed.
If this is the type of a bound variable, return a u64 whose only activated bit is the bit indicating which bv it is.
The POSITION (1 - 55) of this bound variable, NOT the literal u64.
If this is a regular/not-bound variable, return a u64 whose only activated bits are the ones marking the bvs on which it depends.
Assuming this is a regular/not-bound variable, return a u64 whose only activated bits are the ones marking the bvs on which it depends.
Trait Implementations
Auto Trait Implementations
impl RefUnwindSafe for Type
impl UnwindSafe for Type
Blanket Implementations
Mutably borrows from an owned value. Read more