max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2021-11-15 18:47:25 -08:00
parent c67541570f
commit 47956b9b9e
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/typeclass.md
View file

@ -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