forget concept

[Charles-Johnson]

Instead of using the syntax

let a -> a

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