search

leanprover-community / quote4

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

add support for the no-op `generalizing := true` #33

Closed eric-wieser closed 8 months ago

eric-wieser commented 9 months ago

This fixes #29, and gives a clearer error on generalizing := false

gebner commented 8 months ago

Looks good to me! Thank you!