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

chore: fix doc

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-11 09:06:33 -08:00
parent fda7055c1a
commit 3b6ec3bfcc
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/typeclass.md
View file

@ -266,7 +266,7 @@ structure Rational where
inv : den ≠ 0
instance : OfNat Rational n where
ofNat := { num := n, den := 1, inv := decide! }
ofNat := { num := n, den := 1, inv := by decide }
instance : ToString Rational where
toString r := s!"{r.num}/{r.den}"
@ -417,7 +417,7 @@ structure Rational where
@[defaultInstance 1]
instance : OfNat Rational n where
ofNat := { num := n, den := 1, inv := decide! }
ofNat := { num := n, den := 1, inv := by decide }
instance : ToString Rational where
toString r := s!"{r.num}/{r.den}"