Struct LeanPrinter 

pub struct LeanPrinter;

The Lean printer

Implementations

impl LeanPrinter

pub fn printable_item(item: &Item) -> bool

A filter for items blacklisted by the Lean backend : returns false if the item is definitely not printable, but might return true on unsupported items

pub fn render_id(&self, id: &GlobalId) -> String

Render a global id using the Rendering strategy of the Lean printer. Works for both concrete and projector ids. TODO: https://github.com/cryspen/hax/issues/1660

pub fn escape(&self, id: String) -> String

Escapes local identifiers (prefixing reserved keywords with an underscore). TODO: This should be treated directly in the name rendering engine, see https://github.com/cryspen/hax/issues/1630

pub fn render_symbol(&self, symbol: Symbol) -> String

Renders a single symbol, used for anonymous implementations of typeclasses

pub fn render_last(&self, id: &GlobalId) -> String

Renders the last, most local part of an id. Used for named arguments of constructors.

impl LeanPrinter

pub fn arguments<'a, 'b, A: 'a + Clone, D>( &'a self, fields: &'b [(GlobalId, D)], is_record: &bool, ) -> DocBuilder<'a, Self, A>

where &'b D: Pretty<'a, Self, A>,

Prints arguments a variant or constructor of struct, using named or unamed arguments based on the is_record flag. Used for both expressions and patterns

Trait Implementations

impl Default for LeanPrinter

fn default() -> LeanPrinter

Returns the “default value” for a type.

impl<'a, A: 'a> DocAllocator<'a, A> for LeanPrinter

type Doc = BoxDoc<'a, A>

fn alloc(&'a self, doc: Doc<'a, Self::Doc, A>) -> Self::Doc

fn alloc_column_fn( &'a self, f: impl Fn(usize) -> Self::Doc + 'a, ) -> <Self::Doc as DocPtr<'a, A>>::ColumnFn

fn alloc_width_fn( &'a self, f: impl Fn(isize) -> Self::Doc + 'a, ) -> <Self::Doc as DocPtr<'a, A>>::WidthFn

fn alloc_cow(&'a self, doc: BuildDoc<'a, Self::Doc, A>) -> Self::Doc

fn nil(&'a self) -> DocBuilder<'a, Self, A>

Allocate an empty document.

fn fail(&'a self) -> DocBuilder<'a, Self, A>

Fails document rendering immediately.

fn hardline(&'a self) -> DocBuilder<'a, Self, A>

Allocate a single hardline.

fn space(&'a self) -> DocBuilder<'a, Self, A>

fn line(&'a self) -> DocBuilder<'a, Self, A>

A line acts like a \n but behaves like space if it is grouped on a single line.

fn line_(&'a self) -> DocBuilder<'a, Self, A>

Acts like line but behaves like nil if grouped on a single line

fn softline(&'a self) -> DocBuilder<'a, Self, A>

A softline acts like space if the document fits the page, otherwise like line

fn softline_(&'a self) -> DocBuilder<'a, Self, A>

A softline_ acts like nil if the document fits the page, otherwise like line_

fn as_string<U>(&'a self, data: U) -> DocBuilder<'a, Self, A>

where U: Display,

Allocate a document containing the text t.to_string().

fn text<U>(&'a self, data: U) -> DocBuilder<'a, Self, A>

where U: Into<Cow<'a, str>>,

Allocate a document containing the given text.

fn concat<I>(&'a self, docs: I) -> DocBuilder<'a, Self, A>

where I: IntoIterator, <I as IntoIterator>::Item: Pretty<'a, Self, A>,

Allocate a document concatenating the given documents.

fn intersperse<I, S>(&'a self, docs: I, separator: S) -> DocBuilder<'a, Self, A>

where I: IntoIterator, <I as IntoIterator>::Item: Pretty<'a, Self, A>, S: Pretty<'a, Self, A> + Clone,

Allocate a document that intersperses the given separator S between the given documents [A, B, C, ..., Z], yielding [A, S, B, S, C, S, ..., S, Z].

fn column( &'a self, f: impl Fn(usize) -> Self::Doc + 'a, ) -> DocBuilder<'a, Self, A>

Allocate a document that acts differently based on the position and page layout

fn nesting( &'a self, f: impl Fn(usize) -> Self::Doc + 'a, ) -> DocBuilder<'a, Self, A>

Allocate a document that acts differently based on the current nesting level

fn reflow(&'a self, text: &'a str) -> DocBuilder<'a, Self, A>

where Self: Sized, Self::Doc: Clone, A: Clone,

Reflows text inserting softline in place of any whitespace

impl<'a, A: 'a + Clone> Pretty<'a, LeanPrinter, A> for &Vec<Param>

Render parameters, adding a line after each parameter

fn pretty(self, allocator: &'a LeanPrinter) -> DocBuilder<'a, LeanPrinter, A>

Converts self into a document

impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for LeanPrinter

fn generics(&'a self, _: &'b Generics) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Render generics, adding a space after each parameter

const NAME: &'static str = "Lean"

A name for this instance of PrettyAst. Useful for diagnostics and debugging.

fn module(&'a self, module: &'b Module) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn global_id(&'a self, global_id: &'b GlobalId) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn generic_constraint( &'a self, generic_constraint: &'b GenericConstraint, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn generic_param( &'a self, generic_param: &'b GenericParam, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn expr(&'a self, _: &'b Expr) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn arm(&'a self, arm: &'b Arm) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn pat(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn pat_kind(&'a self, pat_kind: &'b PatKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn ty(&'a self, ty: &'b Ty) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn literal(&'a self, literal: &'b Literal) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn local_id(&'a self, local_id: &'b LocalId) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn spanned_ty(&'a self, spanned_ty: &'b SpannedTy) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn primitive_ty( &'a self, primitive_ty: &'b PrimitiveTy, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn int_kind(&'a self, int_kind: &'b IntKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn generic_value( &'a self, generic_value: &'b GenericValue, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn quote_content( &'a self, quote_content: &'b QuoteContent, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn quote(&'a self, quote: &'b Quote) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn param(&'a self, param: &'b Param) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn item(&'a self, item: &'b Item) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn trait_item(&'a self, _: &'b TraitItem) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn impl_item(&'a self, _: &'b ImplItem) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn impl_ident(&'a self, _: &'b ImplIdent) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn trait_goal(&'a self, _: &'b TraitGoal) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn variant(&'a self, _: &'b Variant) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn emit_diagnostic(&'a self, kind: Kind)

Emit a diagnostic with proper context and span.

fn todo_document( &'a self, message: &str, issue_id: Option<u32>, ) -> DocBuilder<'a, Self, A>

Produce a non-panicking placeholder document. In general, prefer the use of the helper macro todo_document!.

fn with_span<T>(&self, span: Span, action: impl Fn(&Self) -> T) -> T

Execute an action with a span hint. Useful for errors.

fn unimplemented_method( &'a self, method: &str, ast: FragmentRef<'_>, ) -> DocBuilder<'a, Self, A>

Produce a structured error document for an unimplemented method.

fn expr_kind(&'a self, expr_kind: &'b ExprKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn ty_kind(&'a self, ty_kind: &'b TyKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn metadata(&'a self, metadata: &'b Metadata) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn lhs(&'a self, lhs: &'b Lhs) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn symbol(&'a self, symbol: &'b Symbol) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn loop_kind(&'a self, loop_kind: &'b LoopKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn safety_kind(&'a self, safety_kind: &'b SafetyKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn binding_mode( &'a self, binding_mode: &'b BindingMode, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn region(&'a self, region: &'b Region) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn impl_expr(&'a self, impl_expr: &'b ImplExpr) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn float_kind(&'a self, float_kind: &'b FloatKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn loop_state(&'a self, loop_state: &'b LoopState) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn control_flow_kind( &'a self, control_flow_kind: &'b ControlFlowKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn dyn_trait_goal( &'a self, dyn_trait_goal: &'b DynTraitGoal, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn attribute(&'a self, attribute: &'b Attribute) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn borrow_kind(&'a self, borrow_kind: &'b BorrowKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn impl_expr_kind( &'a self, impl_expr_kind: &'b ImplExprKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn int_size(&'a self, int_size: &'b IntSize) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn signedness(&'a self, signedness: &'b Signedness) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn guard(&'a self, guard: &'b Guard) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn attribute_kind( &'a self, attribute_kind: &'b AttributeKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn guard_kind(&'a self, guard_kind: &'b GuardKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn impl_item_kind( &'a self, impl_item_kind: &'b ImplItemKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn trait_item_kind( &'a self, trait_item_kind: &'b TraitItemKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn item_quote_origin( &'a self, item_quote_origin: &'b ItemQuoteOrigin, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn item_quote_origin_kind( &'a self, item_quote_origin_kind: &'b ItemQuoteOriginKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn item_quote_origin_position( &'a self, item_quote_origin_position: &'b ItemQuoteOriginPosition, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn generic_param_kind( &'a self, generic_param_kind: &'b GenericParamKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn projection_predicate( &'a self, projection_predicate: &'b ProjectionPredicate, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn doc_comment_kind( &'a self, doc_comment_kind: &'b DocCommentKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn item_kind(&'a self, item_kind: &'b ItemKind) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn error_node(&'a self, error_node: &'b ErrorNode) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn resugared_expr_kind( &'a self, resugared_expr_kind: &'b ResugaredExprKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn resugared_ty_kind( &'a self, resugared_ty_kind: &'b ResugaredTyKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn resugared_pat_kind( &'a self, resugared_pat_kind: &'b ResugaredPatKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn resugared_impl_item_kind( &'a self, resugared_impl_item_kind: &'b ResugaredImplItemKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn resugared_trait_item_kind( &'a self, resugared_trait_item_kind: &'b ResugaredTraitItemKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

fn resugared_item_kind( &'a self, resugared_item_kind: &'b ResugaredItemKind, ) -> DocBuilder<'a, Self, A>

👎Deprecated: Do not call this method directly. Use [pretty::Pretty::pretty] instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use pretty::Pretty::pretty instead, so annotations/spans are preserved correctly.

impl Printer for LeanPrinter

fn resugaring_phases() -> Vec<Box<dyn Resugaring>>

A list of resugaring phases.

const NAME: &'static str = _

The name of the printer

impl RenderView for LeanPrinter

fn separator(&self) -> &str

Returns the string used to join rendered atoms (defaults to "::").

fn render_path_segment(&self, chunk: &PathSegment) -> Vec<String>

Renders a single PathSegment into a vector of display atoms.

fn render_unnamed_path_segment_payload( &self, unnamed: UnnamedPathSegmentPayload, ) -> Symbol

Converts an unnamed path segment payload into a printable Symbol.

fn render_path_segment_payload(&self, payload: PathSegmentPayload) -> Symbol

Converts a full PathSegmentPayload (named or unnamed) into a printable Symbol.

fn module(&self, view: &View) -> Vec<String>

Renders just the module path (crate + modules) of a View, as a list of atoms.

fn render(&self, view: &View) -> Rendered

Renders a View into a structured Rendered value, splitting output into module and path parts.

fn rendered_to_strings( &self, rendered: Rendered, ) -> impl Iterator<Item = String>

Lazy render a view as an iterator of strings.

fn rendered_to_string(&self, rendered: Rendered) -> String

Joins the atoms contained in a Rendered into a single string using separator.

fn render_string(&self, view: &View) -> String

Convenience: renders a View straight to a single String.

fn render_strings(&self, view: &View) -> impl Iterator<Item = String>

Convenience: renders a View straight to a iterator of Strings.