Currently, a ForAll in the context or an Exists in the goal is handled by blindly instantiating the variable with whatever constants are in the context. This is inefficient for some purposes, and can lead to creating ill-typed formulas as well.
One possibility to handle these, for pure values, is to add them into the context as existential variables (think eintros in Coq). Then, they can be unified as necessary, or even left to the SMT solver to process.
Currently, a
ForAllin the context or anExistsin the goal is handled by blindly instantiating the variable with whatever constants are in the context. This is inefficient for some purposes, and can lead to creating ill-typed formulas as well.One possibility to handle these, for pure values, is to add them into the context as existential variables (think
eintrosin Coq). Then, they can be unified as necessary, or even left to the SMT solver to process.