Struct mm0_util::AtomId [−][src]
pub struct AtomId(pub u32);
An index into a AtomVec
Implementations
impl AtomId
[src]
#[must_use]pub fn into_inner(self) -> u32
[src]
Convert this newtyped integer into its underlying integer.
impl AtomId
[src]
pub const UNDER: AtomId
[src]
The atom _
.
The blank, used to represent wildcards in match
pub const BANG: AtomId
[src]
The atom !
.
In refine, (! thm x y e1 e2 p1 p2)
allows passing bound and regular variables,
in addition to subproofs
pub const BANG2: AtomId
[src]
The atom !!
.
In refine, (!! thm x y p1 p2)
allows passing bound variables and subproofs but not
regular variables, in addition to subproofs
pub const VERB: AtomId
[src]
The atom :verb
.
In refine, (:verb p)
allows passing an elaborated proof term p
in a refine script
(without this, the applications in p
would be interpreted incorrectly)
pub const CONV: AtomId
[src]
The atom :conv
.
In elaborated proofs, (:conv e c p)
is a conversion proof.
(The initial colon avoids name collision with MM0 theorems, which don’t allow :
in identifiers.)
pub const SYM: AtomId
[src]
The atom :sym
.
In elaborated proofs, (:sym c)
is a proof of symmetry.
(The initial colon avoids name collision with MM0 theorems, which don’t allow :
in identifiers.)
pub const UNFOLD: AtomId
[src]
The atom :unfold
.
In elaborated proofs, (:unfold t es c)
is a proof of definitional unfolding.
(The initial colon avoids name collision with MM0 theorems, which don’t allow :
in identifiers.)
pub const LET: AtomId
[src]
The atom :let
.
In MMU proofs, (:let h p1 p2)
is a let-binding for supporting deduplication.
pub const COLON: AtomId
[src]
The atom :
.
In refine, {p : t}
is a type ascription for proofs.
pub const QMARK: AtomId
[src]
The atom ?
.
In refine, ?
is a proof by “sorry” (stubbing the proof without immediate error)
pub const TERM: AtomId
[src]
The atom term
.
term
is an atom used by add-decl
to add a term/def declaration
pub const DEF: AtomId
[src]
The atom def
.
def
is an atom used by add-decl
to add a term/def declaration
pub const AXIOM: AtomId
[src]
The atom axiom
.
axiom
is an atom used by add-decl
to add an axiom/theorem declaration
pub const THM: AtomId
[src]
The atom theorem
.
theorem
is an atom used by add-decl
to add an axiom/theorem declaration
pub const PUB: AtomId
[src]
The atom pub
.
pub
is an atom used to specify the visibility modifier in add-decl
pub const ABSTRACT: AtomId
[src]
The atom abstract
.
abstract
is an atom used to specify the visibility modifier in add-decl
pub const LOCAL: AtomId
[src]
The atom local
.
local
is an atom used to specify the visibility modifier in add-decl
pub const SORRY: AtomId
[src]
The atom :sorry
.
:sorry
is an atom used by get-decl
to print missing proofs
pub const ERROR: AtomId
[src]
The atom error
.
error
is an error level recognized by set-reporting
pub const WARN: AtomId
[src]
The atom warn
.
warn
is an error level recognized by set-reporting
pub const INFO: AtomId
[src]
The atom info
.
info
is an error level recognized by set-reporting
pub const ANNOTATE: AtomId
[src]
The atom annotate
.
The annotate
function is a callback used to define what happens when an annotation like
@foo def bar = ...
is used.
pub const REFINE_EXTRA_ARGS: AtomId
[src]
The atom refine-extra-args
.
The refine-extra-args
function is a callback used when an application in refine
uses too many arguments.
pub const TO_EXPR_FALLBACK: AtomId
[src]
The atom to-expr-fallback
.
to-expr-fallback
is called when elaborating a term that is not otherwise recognized
pub fn on_atoms(f: impl FnMut(&str, AtomId))
[src]
Map a function over the list of atom constants (in increasing order).
Trait Implementations
impl Clone for AtomId
[src]
impl Copy for AtomId
[src]
impl Debug for AtomId
[src]
impl DeepSizeOf for AtomId
[src]
fn deep_size_of_children(&self, _: &mut Context) -> usize
[src]
pub fn deep_size_of(&self) -> usize
[src]
pub fn deep_size_of_with(&self, context: &mut Context) -> usize
[src]
impl Default for AtomId
[src]
impl Eq for AtomId
[src]
impl Hash for AtomId
[src]
fn hash<__H: Hasher>(&self, state: &mut __H)
[src]
pub fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
1.3.0[src]
H: Hasher,
impl<T> Index<AtomId> for AtomVec<T>
[src]
impl<T> IndexMut<AtomId> for AtomVec<T>
[src]
impl Ord for AtomId
[src]
fn cmp(&self, other: &AtomId) -> Ordering
[src]
#[must_use]pub fn max(self, other: Self) -> Self
1.21.0[src]
#[must_use]pub fn min(self, other: Self) -> Self
1.21.0[src]
#[must_use]pub fn clamp(self, min: Self, max: Self) -> Self
1.50.0[src]
impl PartialEq<AtomId> for AtomId
[src]
impl PartialOrd<AtomId> for AtomId
[src]
fn partial_cmp(&self, other: &AtomId) -> Option<Ordering>
[src]
#[must_use]pub fn lt(&self, other: &Rhs) -> bool
1.0.0[src]
#[must_use]pub fn le(&self, other: &Rhs) -> bool
1.0.0[src]
#[must_use]pub fn gt(&self, other: &Rhs) -> bool
1.0.0[src]
#[must_use]pub fn ge(&self, other: &Rhs) -> bool
1.0.0[src]
impl StructuralEq for AtomId
[src]
impl StructuralPartialEq for AtomId
[src]
Auto Trait Implementations
impl RefUnwindSafe for AtomId
impl Send for AtomId
impl Sync for AtomId
impl Unpin for AtomId
impl UnwindSafe for AtomId
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Erased for T
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,