chore: annotate OfNat and ToString default instances
This commit is contained in:
parent
84741279c0
commit
b672e37bcc
3 changed files with 10 additions and 0 deletions
|
|
@ -25,6 +25,7 @@ instance {α} [ToString α] : ToString (id α) :=
|
|||
instance {α} [ToString α] : ToString (Id α) :=
|
||||
inferInstanceAs (ToString α)
|
||||
|
||||
@[defaultInstance]
|
||||
instance : ToString String :=
|
||||
⟨fun s => s⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -345,6 +345,7 @@ class OfNat (α : Type u) :=
|
|||
|
||||
export OfNat (ofNat)
|
||||
|
||||
@[defaultInstance]
|
||||
instance : OfNat Nat := ⟨id⟩
|
||||
|
||||
instance : Inhabited Nat := {
|
||||
|
|
|
|||
|
|
@ -167,3 +167,11 @@ def tst8 : MetaM Unit := do
|
|||
pure ()
|
||||
|
||||
#eval tst8
|
||||
|
||||
def tst9 : MetaM Unit := do
|
||||
print "----- tst9 -----"
|
||||
let defInsts ← getDefaultInstances `OfNat
|
||||
print (toString defInsts)
|
||||
pure ()
|
||||
|
||||
#eval tst9
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue