pub struct AxiomBlock {
pub name: String,
pub formula: String,
}Expand description
A ## Axiom block: a named first-order axiom in formal notation.
## Axiom flip: for all a b, Cong(a, b, b, a). registers flip as a shared premise
available to every later theorem in the program — the seam for an axiomatic base like
Tarski geometry.
Fields§
§name: StringThe axiom’s name (flip), for citation and diagnostics.
formula: StringThe axiom formula as surface text, parsed downstream by the formal-formula parser.
Trait Implementations§
Source§impl Clone for AxiomBlock
impl Clone for AxiomBlock
Source§fn clone(&self) -> AxiomBlock
fn clone(&self) -> AxiomBlock
Returns a duplicate of the value. Read more
1.0.0 (const: unstable) · 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 AxiomBlock
impl Debug for AxiomBlock
Source§impl PartialEq for AxiomBlock
impl PartialEq for AxiomBlock
Source§fn eq(&self, other: &AxiomBlock) -> bool
fn eq(&self, other: &AxiomBlock) -> bool
Tests for
self and other values to be equal, and is used by ==.impl Eq for AxiomBlock
impl StructuralPartialEq for AxiomBlock
Auto Trait Implementations§
impl Freeze for AxiomBlock
impl RefUnwindSafe for AxiomBlock
impl Send for AxiomBlock
impl Sync for AxiomBlock
impl Unpin for AxiomBlock
impl UnsafeUnpin for AxiomBlock
impl UnwindSafe for AxiomBlock
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<T> Downcast for Twhere
T: Any,
impl<T> Downcast for Twhere
T: Any,
§fn into_any(self: Box<T>) -> Box<dyn Any>
fn into_any(self: Box<T>) -> Box<dyn Any>
Convert
Box<dyn Trait> (where Trait: Downcast) to Box<dyn Any>. Box<dyn Any> can
then be further downcast into Box<ConcreteType> where ConcreteType implements Trait.§fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>
fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>
Convert
Rc<Trait> (where Trait: Downcast) to Rc<Any>. Rc<Any> can then be
further downcast into Rc<ConcreteType> where ConcreteType implements Trait.§fn as_any(&self) -> &(dyn Any + 'static)
fn as_any(&self) -> &(dyn Any + 'static)
Convert
&Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot
generate &Any’s vtable from &Trait’s.§fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)
fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)
Convert
&mut Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot
generate &mut Any’s vtable from &mut Trait’s.§impl<T> DowncastSync for T
impl<T> DowncastSync for T
§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.