Note: the hardcoding in this patch is only for the 2.2 hotfix branch; in
the 2.3 branch we will only have to change the default setting for the
typechecker.
Revised how we do output for `:sat` and `:prove` without arguments,
making it more clear what properties are being checked in each case.
Also reworded the output of `:check` slightly in the case where the
property has no inputs. It would be nice to make `:check` output more
consistent with the others.
See #66 for more discussion. Basically we don't want the type of `it` to be different for unsat or sat results, so we put undefined values in there instead. Also, instead of using tuples and different field names to distinguish formula arguments of various arities, we use a convention of fields `arg1`, `arg2`, ...
Per @weaversa's suggestions in #66, we now bind records to `it` for sat results, leading to less ambiguity about the meaning of those results. There is still some weirdness to this; the fields present in the record change based on the result and the arity of the formula, but this seems like a reasonable approach given that it's not an expression that needs a type.
Similar to what @weaversa requested in #66, we bind `it` to `False`
when we can't find a sat assignment, and `it` to `True` when we've
proved a theorem.
Also adds some simple tests for the sat/prove result binding, and let
binding at the repl.
