Struct mm0_util::AtomId [−][src]
pub struct AtomId(pub u32);
Expand description
An index into a AtomVec
Tuple Fields
0: u32
Implementations
The atom !
.
In refine, (! thm x y e1 e2 p1 p2)
allows passing bound and regular variables,
in addition to subproofs
The atom !!
.
In refine, (!! thm x y p1 p2)
allows passing bound variables and subproofs but not
regular variables, in addition to subproofs
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)
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.)
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.)
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.)
The atom :let
.
In MMU proofs, (:let h p1 p2)
is a let-binding for supporting deduplication.
The atom ?
.
In refine, ?
is a proof by “sorry” (stubbing the proof without immediate error)
The atom term
.
term
is an atom used by add-decl
to add a term/def declaration
The atom def
.
def
is an atom used by add-decl
to add a term/def declaration
The atom axiom
.
axiom
is an atom used by add-decl
to add an axiom/theorem declaration
The atom theorem
.
theorem
is an atom used by add-decl
to add an axiom/theorem declaration
The atom pub
.
pub
is an atom used to specify the visibility modifier in add-decl
The atom abstract
.
abstract
is an atom used to specify the visibility modifier in add-decl
The atom local
.
local
is an atom used to specify the visibility modifier in add-decl
The atom :sorry
.
:sorry
is an atom used by get-decl
to print missing proofs
The atom annotate
.
The annotate
function is a callback used to define what happens when an annotation like
@foo def bar = ...
is used.
The atom refine-extra-args
.
The refine-extra-args
function is a callback used when an application in refine
uses too many arguments.
The atom to-expr-fallback
.
to-expr-fallback
is called when elaborating a term that is not otherwise recognized
Convert this newtyped integer into its underlying integer.
Trait Implementations
Returns an estimation of the heap-managed storage of this object. This does not include the size of the object itself. Read more
Returns an estimation of a total size of memory owned by the object, including heap-managed storage. Read more
Returns an estimation of a total size of memory owned by the object, including heap-managed storage. Read more
This method returns an ordering between self
and other
values if one exists. Read more
This method tests less than (for self
and other
) and is used by the <
operator. Read more
This method tests less than or equal to (for self
and other
) and is used by the <=
operator. Read more
This method tests greater than (for self
and other
) and is used by the >
operator. Read more
Auto Trait Implementations
impl RefUnwindSafe for AtomId
impl UnwindSafe for AtomId
Blanket Implementations
Mutably borrows from an owned value. Read more