Write a tactic that generalizes a local have or let statement: Given some context and a have or let with a certain type signature, generate a new have / let declaration with all free variables in the context of the have / let introduced as parameters.
- Provide a way to restrict the generalization by explicitly listing the variable that should be generalized.
- Write useful test cases.
Write a tactic that generalizes a local
haveorletstatement: Given some context and ahaveorletwith a certain type signature, generate a newhave/letdeclaration with all free variables in the context of thehave/letintroduced as parameters.