diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 6d588d3d0b..8870ff316c 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -911,7 +911,7 @@ differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like -`_fvar.22` with `_`. +`_fvar.22` with `_fvar._`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index b2940f5c96..7cc2c69e5b 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -51,7 +51,7 @@ def delabFVar : Delab := do -- use internal name like `_fvar.22` maybeAddBlockImplicit <| mkIdent (fvarId.name.replacePrefix `_uniq `_fvar) else - maybeAddBlockImplicit <| mkIdent `_ + maybeAddBlockImplicit <| mkIdent `_fvar._ -- loose bound variable, use pseudo syntax @[builtin_delab bvar] diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean index 1ee6a9b6bb..4475cbe095 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Options.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean @@ -133,7 +133,7 @@ register_builtin_option pp.mvars.delayed : Bool := { register_builtin_option pp.fvars.anonymous : Bool := { defValue := true descr := "(pretty printer) display names for loose free variables (not in the local context) such as `_fvar.22` when true, \ - and otherwise display them as '_'. Useful for stabilizing output in `#guard_msgs`." + and otherwise display them as `_fvar._`. Useful for stabilizing output in `#guard_msgs`." } register_builtin_option pp.beta : Bool := { defValue := false diff --git a/tests/lean/run/ppFVarsAnonymous.lean b/tests/lean/run/ppFVarsAnonymous.lean index 9a1d4f77a1..ee79e8ecef 100644 --- a/tests/lean/run/ppFVarsAnonymous.lean +++ b/tests/lean/run/ppFVarsAnonymous.lean @@ -6,7 +6,7 @@ import Lean When a free variable is not in the local context (a "loose" fvar), the pretty printer renders it with an internal name like `_fvar.42`. The `pp.fvars.anonymous` option (default `true`) controls this behavior: -when set to `false`, loose fvars are displayed as `_`. +when set to `false`, loose fvars are displayed as `_fvar._`. -/ open Lean Elab Command in @@ -24,4 +24,4 @@ run_cmd liftTermElabM do let fvarId : FVarId := { name := .num `_uniq 42 } let e := Expr.fvar fvarId let fmt ← Meta.ppExpr e - guard <| s!"{fmt}" == "_" + guard <| s!"{fmt}" == "_fvar._"