From 27158eb3e29d0fcb3c61193e1a6ada911e98e500 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Wed, 8 Jan 2020 13:14:35 -0500 Subject: [PATCH] fix: DiscrTree typos --- src/Init/Lean/Meta/DiscrTree.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Meta/DiscrTree.lean b/src/Init/Lean/Meta/DiscrTree.lean index f7e2a11f30..96f47a7762 100644 --- a/src/Init/Lean/Meta/DiscrTree.lean +++ b/src/Init/Lean/Meta/DiscrTree.lean @@ -42,7 +42,7 @@ namespace DiscrTree That is, we don't reduce `HasAdd.add Nat Nat.HasAdd a b` into `Nat.add a b`. We say the `HasAdd.add` applications are the de-facto canonical forms in the metaprogramming framework. - Moreover, it is the metaprammer resposability to re-pack applications such as + Moreover, it is the metaprogrammer's responsibility to re-pack applications such as `Nat.add a b` into `HasAdd.add Nat Nat.hasAdd a b`. Remark: we store the arity in the keys