diff --git a/doc/typeclass.md b/doc/typeclass.md index 5471739c5f..36fd4d227c 100644 --- a/doc/typeclass.md +++ b/doc/typeclass.md @@ -423,8 +423,6 @@ instance : ToString Rational where toString r := s!"{r.num}/{r.den}" #check 2 -- Rational - -example ``` Priorities are also useful to control the interaction between different default instances. For example, suppose `xs` has type `α`, when elaboration `xs.map (fun x => 2 * x)`, we want the homogeneous instance for multiplication