source
def ProofWidgets.Util.joinArrays {m : Type → Type} [Monad m] [Lean.MonadRef m] [Lean.MonadQuotation m] (arr : Array Lean.Term) :
m Lean.Term

Sends `#[a, b, c]` to ``(term| $a ++ $b ++ $c)`

Equations

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

Instances For

source
def ProofWidgets.Util.foldInlsM {α β : Type u_1} {m : Type u_1 → Type u_2} [Monad m] (arr : Array (α ⊕ β)) (f : Array α → m β) :
m (Array β)

Collapse adjacent `inl (_ : α)`s into a `β` using `f`. For example, `#[.inl a₁, .inl a₂, .inr b, .inl a₃] ↦ #[← f #[a₁, a₂], b, ← f #[a₃]]`.

Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.delabListLiteral {α : Type} (elem : DelabM α) :
DelabM (Array α)

Delaborate the elements of a list literal separately, calling `elem` on each.

Equations

- Lean.PrettyPrinter.Delaborator.delabListLiteral elem = Lean.PrettyPrinter.Delaborator.delabListLiteral.go✝ elem #[]

Instances For

source
def Lean.PrettyPrinter.Delaborator.delabArrayLiteral {α : Type} (elem : DelabM α) :
DelabM (Array α)

Delaborate the elements of an array literal separately, calling `elem` on each.

Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.annotateTermLikeInfo {n : SyntaxNodeKinds} (stx : TSyntax n) :
DelabM (TSyntax n)

A copy of `Delaborator.annotateTermInfo` for other syntactic categories.

Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.withAnnotateTermLikeInfo {n : SyntaxNodeKinds} (d : DelabM (TSyntax n)) :
DelabM (TSyntax n)

A copy of `Delaborator.withAnnotateTermInfo` for other syntactic categories.

Equations

- Lean.PrettyPrinter.Delaborator.withAnnotateTermLikeInfo d = do let stx ← d Lean.PrettyPrinter.Delaborator.annotateTermLikeInfo stx

Instances For