From ddf77a8c6d6c1a754e695cd1c67ddc8685abda2c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 30 Jun 2022 13:21:26 +0200 Subject: [PATCH] chore: style --- src/Init/Meta.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 96bb09674c..97e1625f27 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -862,7 +862,7 @@ class Quote (α : Type) (k : SyntaxNodeKind := `term) where export Quote (quote) -instance [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])]: Quote α k' := ⟨fun a => quote (k := k) a⟩ +instance [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])] : Quote α k' := ⟨fun a => quote (k := k) a⟩ instance : Quote Term := ⟨id⟩ instance : Quote Bool := ⟨fun | true => mkCIdent `Bool.true | false => mkCIdent `Bool.false⟩