Struct AtomId

pub struct AtomId(pub u32);

An index into a AtomVec

Tuple Fields

0: u32

Implementations

impl AtomId

pub const UNDER: AtomId

The atom _. The blank, used to represent wildcards in match

pub const BANG: AtomId

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

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

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

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

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

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

The atom :let. In MMU proofs, (:let h p1 p2) is a let-binding for supporting deduplication.

pub const COLON: AtomId

The atom :. In refine, {p : t} is a type ascription for proofs.

pub const QMARK: AtomId

The atom ?. In refine, ? is a proof by “sorry” (stubbing the proof without immediate error)

pub const TERM: AtomId

The atom term. term is an atom used by add-decl to add a term/def declaration

pub const DEF: AtomId

The atom def. def is an atom used by add-decl to add a term/def declaration

pub const AXIOM: AtomId

The atom axiom. axiom is an atom used by add-decl to add an axiom/theorem declaration

pub const THM: AtomId

The atom theorem. theorem is an atom used by add-decl to add an axiom/theorem declaration

pub const PUB: AtomId

The atom pub. pub is an atom used to specify the visibility modifier in add-decl

pub const ABSTRACT: AtomId

The atom abstract. abstract is an atom used to specify the visibility modifier in add-decl

pub const LOCAL: AtomId

The atom local. local is an atom used to specify the visibility modifier in add-decl

pub const SORRY: AtomId

The atom :sorry. :sorry is an atom used by get-decl to print missing proofs

pub const ERROR: AtomId

The atom error. error is an error level recognized by set-reporting

pub const WARN: AtomId

The atom warn. warn is an error level recognized by set-reporting

pub const INFO: AtomId

The atom info. info is an error level recognized by set-reporting

pub const ANNOTATE: AtomId

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

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

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))

Map a function over the list of atom constants (in increasing order).

impl AtomId

pub fn into_inner(self) -> u32

Convert this newtyped integer into its underlying integer.

Trait Implementations

impl Clone for AtomId

fn clone(&self) -> AtomId

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for AtomId

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl DeepSizeOf for AtomId

fn deep_size_of_children(&self, _: &mut Context) -> usize

Returns an estimation of the heap-managed storage of this object. This does not include the size of the object itself.

fn deep_size_of(&self) -> usize

Returns an estimation of a total size of memory owned by the object, including heap-managed storage.

fn deep_size_of_with(&self, context: &mut Context) -> usize

Returns an estimation of a total size of memory owned by the object, including heap-managed storage.

impl Default for AtomId

fn default() -> AtomId

Returns the “default value” for a type.

impl Hash for AtomId

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<T> Index<AtomId> for AtomVec<T>

type Output = T

The returned type after indexing.

fn index(&self, i: AtomId) -> &T

Performs the indexing (container[index]) operation.

impl<T> IndexMut<AtomId> for AtomVec<T>

fn index_mut(&mut self, i: AtomId) -> &mut T

Performs the mutable indexing (container[index]) operation.

impl Ord for AtomId

fn cmp(&self, other: &AtomId) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for AtomId

fn eq(&self, other: &AtomId) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for AtomId

fn partial_cmp(&self, other: &AtomId) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Copy for AtomId

impl Eq for AtomId

impl StructuralPartialEq for AtomId