Open Charles-Johnson opened 3 years ago
Now that #20 has been resolved, it should be possible to
let ((_y_ exists_such_that) (_x_ -> _y_) and _y_ -> _z_) => _x_ -> _z_
which would remove the need for ContextSearch::recursively_reduce.
ContextSearch::recursively_reduce
This will allow the interpreter to reason more generally.
One could go further and generalise the transitive properties shared with comparison and reduction with the statements
let (_o_ is transitive) => ((_y_ exists_such_that) (_x_ _o_ _y_) and _y_ _o_ _z_) => _x_ _o_ _z_
and
let -> is transitive
let > is transitive
This will be a good test for the reasoning of the interpreter
I should open a PR testing this
Now that #20 has been resolved, it should be possible to
which would remove the need for
ContextSearch::recursively_reduce
.This will allow the interpreter to reason more generally.
One could go further and generalise the transitive properties shared with comparison and reduction with the statements
and
and
This will be a good test for the reasoning of the interpreter