Gergely Buday (Aug 14 2024 at 12:03): Gergely Buday (Aug 14 2024 at 12:03):What does it mean to have an
Illegal dummy pattern(s) in term
?
Mathias Fleury (Aug 14 2024 at 12:39):I mostly see that when using find_theorems in a place where a name is required (like a lambda abstraction)
Mathias Fleury (Aug 14 2024 at 12:40):the error message means that you have an underscore where it is not allowed. Replace the _ by a name and the error will be gone
Last updated: Dec 21 2024 at 12:33 UTC