§ Lean4 access metam and so forth

#eval show Lean.MetaM _ from do
  return 0