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
Instances For
A copy of Delaborator.annotateTermInfo
for other syntactic categories.
Equations
Instances For
def
Lean.PrettyPrinter.Delaborator.withAnnotateTermLikeInfo
{n : SyntaxNodeKinds}
(d : DelabM (TSyntax n))
:
A copy of Delaborator.withAnnotateTermInfo
for other syntactic categories.