pub struct AtomId(pub u32);
Expand description
An index into a AtomVec
Tuple Fields§
§0: u32
Implementations§
Source§impl AtomId
impl AtomId
Sourcepub const BANG: AtomId
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
Sourcepub const BANG2: AtomId
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
Sourcepub const VERB: AtomId
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)
Sourcepub const CONV: AtomId
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.)
Sourcepub const SYM: AtomId
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.)
Sourcepub const UNFOLD: AtomId
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.)
Sourcepub const LET: AtomId
pub const LET: AtomId
The atom :let
.
In MMU proofs, (:let h p1 p2)
is a let-binding for supporting deduplication.
Sourcepub const QMARK: AtomId
pub const QMARK: AtomId
The atom ?
.
In refine, ?
is a proof by “sorry” (stubbing the proof without immediate error)
Sourcepub const TERM: AtomId
pub const TERM: AtomId
The atom term
.
term
is an atom used by add-decl
to add a term/def declaration
Sourcepub const DEF: AtomId
pub const DEF: AtomId
The atom def
.
def
is an atom used by add-decl
to add a term/def declaration
Sourcepub const AXIOM: AtomId
pub const AXIOM: AtomId
The atom axiom
.
axiom
is an atom used by add-decl
to add an axiom/theorem declaration
Sourcepub const THM: AtomId
pub const THM: AtomId
The atom theorem
.
theorem
is an atom used by add-decl
to add an axiom/theorem declaration
Sourcepub const PUB: AtomId
pub const PUB: AtomId
The atom pub
.
pub
is an atom used to specify the visibility modifier in add-decl
Sourcepub const ABSTRACT: AtomId
pub const ABSTRACT: AtomId
The atom abstract
.
abstract
is an atom used to specify the visibility modifier in add-decl
Sourcepub const LOCAL: AtomId
pub const LOCAL: AtomId
The atom local
.
local
is an atom used to specify the visibility modifier in add-decl
Sourcepub const SORRY: AtomId
pub const SORRY: AtomId
The atom :sorry
.
:sorry
is an atom used by get-decl
to print missing proofs
Sourcepub const ANNOTATE: AtomId
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.
Sourcepub const REFINE_EXTRA_ARGS: AtomId
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.
Sourcepub const TO_EXPR_FALLBACK: AtomId
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