surprising behavior of `trivial`

Stream: lean4

[Eric Wieser]

This did not behave as expected:

-- produces a crazy term
#check by trivial

[Aaron Liu]

Without an expected type nothing's stopping it from doing everything

[Eric Wieser]

I guess

macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)

is to blame; it probably shouldn't be willing to assign metavariables