Trait LeanFmt 

pub trait LeanFmt {
    // Required method
    fn lean_fmt(
        &self,
        f: &mut Formatter<'_>,
        cx: &LeanCtxt<'_, '_, '_>,
    ) -> Result;
}

Required Methods

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

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl LeanFmt for (&KVid, &ClosedSolution)

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

impl LeanFmt for [Pred]

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

impl<T: LeanFmt> LeanFmt for &T

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

Implementors

impl LeanFmt for Constraint

impl LeanFmt for DataDecl

impl LeanFmt for DataField

impl LeanFmt for DataSort

impl LeanFmt for Expr

impl LeanFmt for FunDef

impl LeanFmt for FunSort

impl LeanFmt for InterpretedConst

impl LeanFmt for KVarDecl

impl LeanFmt for LeanAdt

impl LeanFmt for LeanDataProj

impl LeanFmt for LeanField

impl LeanFmt for Pred

impl LeanFmt for Sort

impl LeanFmt for SortDecl

impl LeanFmt for Var

impl<'a> LeanFmt for LeanKConstraint<'a>