From a406e41fcbc5dcd8dda695c1a93d85b63e0738b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Mar 2021 18:11:06 -0800 Subject: [PATCH] chore: fix documentation --- doc/typeclass.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/typeclass.md b/doc/typeclass.md index 06a39eba0d..2fb85a6308 100644 --- a/doc/typeclass.md +++ b/doc/typeclass.md @@ -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 α] : α :=