From 141b110ff10e8351f5ce38899607b48bd3bb418d Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 30 Jun 2022 13:43:13 +0200 Subject: [PATCH] feat: add more typed syntax coercions --- src/Init/Meta.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 9eae79ee2c..76586e495d 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -287,6 +287,12 @@ instance : Coe NumLit Term where instance : Coe CharLit Term where coe s := ⟨s.raw⟩ +instance : Coe Ident Syntax.Level where + coe s := ⟨s.raw⟩ + +instance : Coe NumLit Prio where + coe s := ⟨s.raw⟩ + instance : Coe NumLit Prec where coe s := ⟨s.raw⟩