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

chore: fix documentation

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

6
doc/typeclass.md
View file

@ -280,9 +280,9 @@ Lean elaborate the terms `(2 : Nat)` and `(2 : Rational)` as
`OfNat.ofNat Nat 2 (instOfNatNat 2)` and
`OfNat.ofNat Rational 2 (instOfNatRational 2)` respectively.
We say the numerals `2` occurring in the elaborated terms are *raw* natural numbers.
You can input the raw natural number `2` using the macro `natLit! 2`.
You can input the raw natural number `2` using the macro `nat_lit 2`.
```lean
#check natLit! 2 -- Nat
#check nat_lit 2 -- Nat
```
Raw natural numbers are *not* polymorphic.
@ -293,7 +293,7 @@ class Monoid (α : Type u) where
unit : α
op : α → α → α
instance [s : Monoid α] : OfNat α (natLit! 1) where
instance [s : Monoid α] : OfNat α (nat_lit 1) where
ofNat := s.unit
def getUnit [Monoid α] : α :=