# Documentation

Lean.PrettyPrinter.Delaborator.Builtins

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations

Return array with n-th element set to kind of n-th parameter of e.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

State for delabAppMatch and helpers.

Instances For

Delaborate applications of "matchers" such as

List.map.match_1 : {α : Type _} →
(motive : List α → Sort _) →
(x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
→
(motive : List α → Sort _) →
(x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
→ Sort _) →
(x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
→
(x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
→ (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
→ motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
→ ((a : α) → (as : List α) → motive (a :: as)) → motive x
→ (as : List α) → motive (a :: as)) → motive x
→ motive (a :: as)) → motive x
→ motive x

Equations
• One or more equations did not get rendered due to their size.

Delaborate applications of the form (fun x => b) v as let_fun x := v; b

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

Check for a Syntax.ident of the given name anywhere in the tree. This is usually a bad idea since it does not check for shadowing bindings, but in the delaborator we assume that bindings are never shadowed.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

Delaborate a projection primitive. These do not usually occur in user code, but are pretty-printed when e.g. #printing a projection function.

Equations
• One or more equations did not get rendered due to their size.

Delaborate a call to a projection function such as Prod.fst.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

Pretty-prints a constant c as c.{} <params> : .

Equations
• One or more equations did not get rendered due to their size.
partial def Lean.PrettyPrinter.Delaborator.delabConstWithSignature.delabParams (idStx : Lean.Ident) (groups : Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder) (curIds : ) :