to "forget" the reduction of a, a new concrete concept, forget can be used.
forget a
Then the following can be defined
let (let true) -> redundant
let (let false) -> contradiction
let (_x_ -> _x_) -> false
Before each let command is executed, the syntax should be reduced. If it reduces to a non-let command, then the reduction is printed, otherwise the original expression in the let command is set to reduce to true (printing "okay" after this concept is implemented in another task).
This means that the cache doesn't need to be invalidated on executing any let commands. Instead forget should trigger cache invalidation that could be selective by determining which reductions were predicated on the forgotten concept. This will be possible to implement after #54
Instead of using the syntax
to "forget" the reduction of
a
, a new concrete concept,forget
can be used.Then the following can be defined
Before each
let
command is executed, the syntax should be reduced. If it reduces to a non-let
command, then the reduction is printed, otherwise the original expression in thelet
command is set to reduce totrue
(printing "okay" after this concept is implemented in another task).This means that the cache doesn't need to be invalidated on executing any
let
commands. Insteadforget
should trigger cache invalidation that could be selective by determining which reductions were predicated on the forgotten concept. This will be possible to implement after #54