search

leanprover-community / lean4-metaprogramming-book

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

doc(lean/main/dsls.lean): fix double error #27

Closed adomani closed 2 years ago

adomani commented 2 years ago

... and, on the way, mention the existence of ..

arthurpaulino commented 2 years ago

While I think this is an interesting and peculiar behavior, the double processing needs better fix. I will work on it later today. It will require a rather deep refactor on the chapter