def
ProofWidgets.Util.joinArrays
{m : Type → Type}
[Monad m]
[Lean.MonadRef m]
[Lean.MonadQuotation m]
(arr : Array 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
def
ProofWidgets.Util.foldInlsM
{α : Type u_1}
{β : 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
def
Lean.PrettyPrinter.Delaborator.delabListLiteral
{α : Type}
(elem : Lean.PrettyPrinter.Delaborator.DelabM α)
:
Delaborate the elements of a list literal separately, calling elem on each.
Equations
Instances For
partial def
Lean.PrettyPrinter.Delaborator.delabListLiteral.go
{α : Type}
(elem : Lean.PrettyPrinter.Delaborator.DelabM α)
(acc : Array α)
:
def
Lean.PrettyPrinter.Delaborator.delabArrayLiteral
{α : Type}
(elem : Lean.PrettyPrinter.Delaborator.DelabM α)
:
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
def
Lean.PrettyPrinter.Delaborator.annotateTermLikeInfo
{n : Lean.SyntaxNodeKinds}
(stx : Lean.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
def
Lean.PrettyPrinter.Delaborator.withAnnotateTermLikeInfo
{n : Lean.SyntaxNodeKinds}
(d : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax n))
:
A copy of Delaborator.withAnnotateTermInfo for other syntactic categories.