Documentation

ProofWidgets.Util

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

Equations
    Instances For
      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
        Instances For

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

          Equations
            Instances For

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

              Equations
                Instances For

                  A copy of Delaborator.annotateTermInfo for other syntactic categories.

                  Equations
                    Instances For

                      A copy of Delaborator.withAnnotateTermInfo for other syntactic categories.

                      Equations
                        Instances For