leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204 stars 47 forks source link

Typo in metavariable example #118

Closed bernborgess closed 4 months ago

bernborgess commented 8 months ago

When ?b was updated to f a, we expect the metavariable ?m3 to be updated from ?b = a to f a = a