You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We know how to invert the function and find the list of values of s such that String.isPrefix s "abcd" will return true. In fact it's a property of the String.isPrefix function.
So, we allow functions to declare inverters. In this case, the String.isPrefix function accepts the argument pattern "f a0 a1", and if argument 0 is the goal - the variable whose possible values we wish to enumerate - then we can generate the expression prefixesOf a1.
At first only built-in functions will be able to declare inverters. But later we will allow user-defined functions to define them. We may also convert existing logic - e.g. that a0 elem a1 can be inverted and a1 is the list of possible values of a0 - into inverters.
The text was updated successfully, but these errors were encountered:
Consider the query
We know how to invert the function and find the list of values of
s
such thatString.isPrefix s "abcd"
will returntrue
. In fact it's a property of theString.isPrefix
function.So, we allow functions to declare inverters. In this case, the
String.isPrefix
function accepts the argument pattern "f a0 a1", and if argument 0 is the goal - the variable whose possible values we wish to enumerate - then we can generate the expressionprefixesOf a1
.At first only built-in functions will be able to declare inverters. But later we will allow user-defined functions to define them. We may also convert existing logic - e.g. that
a0 elem a1
can be inverted anda1
is the list of possible values ofa0
- into inverters.The text was updated successfully, but these errors were encountered: