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

fix: DiscrTree typos

Browse source
This commit is contained in:
Daniel Selsam 2020-01-08 13:14:35 -05:00 • committed by Leonardo de Moura
parent c5111de0f0
commit 27158eb3e2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Meta/DiscrTree.lean
View file

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