search

leanprover-community / lean4-metaprogramming-book

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

Change to delayed mvar assignments #62

Closed JLimperg closed 1 year ago

JLimperg commented 2 years ago

The mechanism used for delayed mvar assignments has changed in a recent nightly. We have a brief section on this in the MetaM chapter, so we should check whether the changes affect our content there. I'll do this at some point, but I wanted to leave a note here so that I'm less likely to forget.

JLimperg commented 1 year ago

Checked this; no changes required.