From 544a04667850db36c94351762fdff77d5c32ea2f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 27 Jun 2022 17:47:57 +0200 Subject: [PATCH] chore: use Syntax.Level --- src/Lean/Level.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index eeea31779f..cd39ec318d 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -447,8 +447,8 @@ mutual | Result.imaxNode fs, r => parenIfFalse (Format.group <| "imax" ++ formatLst fs) r end -protected partial def Result.quote (r : Result) (prec : Nat) : TSyntax `level := - let addParen (s : TSyntax `level) := +protected partial def Result.quote (r : Result) (prec : Nat) : Syntax.Level := + let addParen (s : Syntax.Level) := if prec > 0 then Unhygienic.run `(level| ( $s )) else s match r with | Result.leaf n => Unhygienic.run `(level| $(mkIdent n):ident) @@ -469,7 +469,7 @@ instance : ToFormat Level where instance : ToString Level where toString u := Format.pretty (Level.format u) -protected def quote (u : Level) (prec : Nat := 0) : TSyntax `level := +protected def quote (u : Level) (prec : Nat := 0) : Syntax.Level := (PP.toResult u).quote prec instance : Quote Level `level where