pub struct Profile {
pub lean_version: &'static str,
pub format_version: &'static str,
pub exporter_name: &'static str,
pub exporter_version: &'static str,
pub allowed_axioms: &'static [&'static str],
}Expand description
The toolchain and assumption profile a result is produced under.
Fields§
§lean_version: &'static str§format_version: &'static str§exporter_name: &'static str§exporter_version: &'static str§allowed_axioms: &'static [&'static str]The assumptions a verified result may depend on, by Lean name.
Trait Implementations§
impl Copy for Profile
impl Eq for Profile
impl StructuralPartialEq for Profile
Auto Trait Implementations§
impl Freeze for Profile
impl RefUnwindSafe for Profile
impl Send for Profile
impl Sync for Profile
impl Unpin for Profile
impl UnsafeUnpin for Profile
impl UnwindSafe for Profile
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