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⟩