Documentation

ProofWidgets.Util

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 : Lean.PrettyPrinter.Delaborator.DelabM α) :
      Lean.PrettyPrinter.Delaborator.DelabM (Array α)

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

      Equations
      Instances For
        source
        partial def Lean.PrettyPrinter.Delaborator.delabListLiteral.go {α : Type} (elem : Lean.PrettyPrinter.Delaborator.DelabM α) (acc : Array α) :
        Lean.PrettyPrinter.Delaborator.DelabM (Array α)
        source
        def Lean.PrettyPrinter.Delaborator.delabArrayLiteral {α : Type} (elem : Lean.PrettyPrinter.Delaborator.DelabM α) :
        Lean.PrettyPrinter.Delaborator.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 : Lean.SyntaxNodeKinds} (stx : Lean.TSyntax n) :
          Lean.PrettyPrinter.Delaborator.DelabM (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
            source
            def Lean.PrettyPrinter.Delaborator.withAnnotateTermLikeInfo {n : Lean.SyntaxNodeKinds} (d : Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax n)) :
            Lean.PrettyPrinter.Delaborator.DelabM (Lean.TSyntax n)

            A copy of Delaborator.withAnnotateTermInfo for other syntactic categories.

            Equations
            Instances For