diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean index a32deb8392..c15310a2b2 100644 --- a/tests/lean/run/doNotation1.lean +++ b/tests/lean/run/doNotation1.lean @@ -2,7 +2,7 @@ open Lean partial def expandHash : Syntax → StateT Bool MacroM Syntax | Syntax.node k args => - if k == `doHash then do set true; `(←MonadState.get) + if k == `doHash then do set true; `(←HasGet.get) else do args ← args.mapM expandHash; pure $ Syntax.node k args