search

leanprover-community / quote4

Intuitive, type-safe expression quotations for Lean 4.
Apache License 2.0
73 stars 11 forks source link

fix: workaround leanprover/lean4#3827 #41

Closed eric-wieser closed 5 months ago

eric-wieser commented 5 months ago

Once it lands in a release, the change in leanprover/lean4#3820 (which detect accidental do lifting in ifs) misfires on quotations (leanprover/lean4#3827). To avoid breakage later, we manually lift out this expression.

semorrison commented 5 months ago

I've checked this works on nightly-2024-04-02. Thanks @eric-wieser!