pub enum InternalFuncKind {
Val(BinOp),
Rel(BinOp),
CharToInt,
IntToChar,
}
Expand description
§Primitive Properties
Given a primop op
with signature (t1,...,tn) -> t
We define a refined type for op
expressed as a RuleMatcher
op :: (x1: t1, ..., xn: tn) -> { t[op_val[op](x1,...,xn)] | op_rel[x1,...,xn] }
That is, using two uninterpreted functions op_val
and op_rel
that respectively denote
- The value of the primop, and
- Some invariant relation that holds for the primop.
The latter can be extended by the user via a property
definition, which allows us
to customize primops like <<
with extra “facts” or lemmas. See tests/tests/pos/surface/primops00.rs
for an example.
Variants§
Val(BinOp)
UIF representing the value of a primop
Rel(BinOp)
UIF representing the relationship of a primop
CharToInt
IntToChar
Trait Implementations§
Source§impl Clone for InternalFuncKind
impl Clone for InternalFuncKind
Source§fn clone(&self) -> InternalFuncKind
fn clone(&self) -> InternalFuncKind
Returns a duplicate of the value. Read more
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source
. Read moreSource§impl Debug for InternalFuncKind
impl Debug for InternalFuncKind
Source§impl<'tcx, __D: TyDecoder<'tcx>> Decodable<__D> for InternalFuncKind
impl<'tcx, __D: TyDecoder<'tcx>> Decodable<__D> for InternalFuncKind
Source§impl<'tcx, __E: TyEncoder<'tcx>> Encodable<__E> for InternalFuncKind
impl<'tcx, __E: TyEncoder<'tcx>> Encodable<__E> for InternalFuncKind
Source§impl From<InternalFuncKind> for Expr
impl From<InternalFuncKind> for Expr
Source§fn from(kind: InternalFuncKind) -> Self
fn from(kind: InternalFuncKind) -> Self
Converts to this type from the input type.
Source§impl Hash for InternalFuncKind
impl Hash for InternalFuncKind
Source§impl PartialEq for InternalFuncKind
impl PartialEq for InternalFuncKind
Source§impl Pretty for InternalFuncKind
impl Pretty for InternalFuncKind
impl Eq for InternalFuncKind
impl StructuralPartialEq for InternalFuncKind
Auto Trait Implementations§
impl Freeze for InternalFuncKind
impl RefUnwindSafe for InternalFuncKind
impl Send for InternalFuncKind
impl Sync for InternalFuncKind
impl Unpin for InternalFuncKind
impl UnwindSafe for InternalFuncKind
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Checks if this value is equivalent to the given key. Read more
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Compare self to
key
and return true
if they are equal.§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Checks if this value is equivalent to the given key. Read more
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self
into a Left
variant of Either<Self, Self>
if into_left
is true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self
into a Left
variant of Either<Self, Self>
if into_left(&self)
returns true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read more