#eval show Lean.MetaM _ from do  return 0