This allows the error to be caught before the blueprint being sent to `leanblueprint` (which would raise a max recursion depth error anyway). This would be implemented in Output.lean using commented out logic in Attribute.lean.
This allows the error to be caught before the blueprint being sent to
leanblueprint(which would raise a max recursion depth error anyway).This would be implemented in Output.lean using commented out logic in Attribute.lean.