ppExpr and pp.mvars

Stream: lean4

[Tomas Skrivan]

How do I call ppExpr with pp.mvars option set to false?

This does not work

import Lean

open Lean Meta
run_meta
  let e ← mkFreshExprMVar (some (Expr.const ``Nat []))
  let s ← withOptions (fun opt => opt.setBool ``pp.mvars false) do ppExpr e
  IO.println s

[Floris van Doorn]

I do not quite understand why, but either of these work:

import Lean

open Lean Meta
run_meta
  let e ← mkFreshExprMVar (some (Expr.const ``Nat []))
  let s ← withOptions (fun opt => opt.setBool `pp.mvars false) do ppExpr e
  withOptions (fun opt => opt.setBool `pp.mvars false) do IO.println s

run_meta
  let e ← mkFreshExprMVar (some (Expr.const ``Nat []))
  withOptions (fun opt => opt.setBool `pp.mvars false) do
    let s ← ppExpr e
    IO.println s

[Tomas Skrivan]

Ohh the original works when you replace

``pp.mvars

with

`pp.mvars

[Eric Wieser]

withOptions (fun opt => pp.mvars.set opt false) is the correct spelling