Closed-form DSL

Stream: lean4

[Leni Aniva]

Is there a DSL to enforce closed-formedness of a function?

In some theorem proving benchmarks like PutnamBench, removing the closed form constraint makes the question trivial.