max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use Syntax.Level

Browse source
This commit is contained in:
Sebastian Ullrich 2022-06-27 17:47:57 +02:00
parent 22475b8669
commit 544a046678
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Level.lean
View file

@ -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