search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Feature: Assume arbitrary number of formulae at once #165

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

< title here again />

assume(f1, f2, f3, ...)

Earlier, they had to each call assume once.

The other versions of assume had to be removed due to currently unresolved overloading issues. Ideally, we would like to have a second version accepting Iterable[Formula], but that case can be handled with the current Formula*. The String version is unused and causes an overload error, so removed it. The string should be explicitly cast to Formula if one wishes to assume it.

sankalpgambhir commented 1 year ago

@dhalilov this may be quite useful for you too