Elaboration check at command level only

[siddhartha-gadgil]

There is a spurious error in the following example, as noted by @Mal-Pat.

{"parsed":
     {"text":
      "∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]\n  {f : β → γ} {g : α → β},\n  UniformContinuous f → UniformContinuous g → UniformContinuous (f ∘ g)",
      "elabError":
      "stuck at solving universe constraint\n  v =?= max u ?u.26708354\nwhile trying to unify\n  Set.{max ?u.26708354 u} (Prod.{u, ?u.26708354} E ?m.26708782) : Type (max ?u.26708354 u)\nwith\n  Set (Prod.{u, ?u.26708354} E ?m.26708782) : Type v ; identifiers [α, u, β, v, γ, w, inst, UniformSpace, α, inst_1, UniformSpace, β, inst_2, UniformSpace, γ, f, β, γ, g, α, β, UniformContinuous, f, UniformContinuous, g, UniformContinuous, f, g] (during elaboration) for ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]\n  {f : β → γ} {g : α → β},\n  UniformContinuous f → UniformContinuous g → UniformContinuous (f ∘ g)",
      "context?":
      "A uniformly continuous function of a uniformly continuous function is uniformly continuous.",
      "cmdErrors": []}}

This can be avoided by checking command elaboration only.

[siddhartha-gadgil]

For comparison, we need not just a check but an elaboration result. This needs some more code: run a named theorem and retrieve the definition.

[siddhartha-gadgil]

closed with 9d6ad35