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
In the command line interface of Kananaskis-11 and a recent development version (7389ca0) “∀x::{x}. T” and “RES_FORALL {x} λx. T” are printed as “∀x::{x}. T” with both instances of “x” shown in green (i.e.: bound). I tested this in Emacs with the HOL interface in Kananaskis-11 and the result is the same (both instances of “x” shown in green).
The text was updated successfully, but these errors were encountered:
This bug has the free-bound status of the restricted variable
contaminate the free/bound status of variables within the restriction.
The printer is also too keen to see restrictions as identical when
they are not because the freeness of variables within the restrictions
are different.
In the command line interface of Kananaskis-11 and a recent development version (7389ca0) “∀x::{x}. T” and “RES_FORALL {x} λx. T” are printed as “∀x::{x}. T” with both instances of “x” shown in green (i.e.: bound). I tested this in Emacs with the HOL interface in Kananaskis-11 and the result is the same (both instances of “x” shown in green).
The text was updated successfully, but these errors were encountered: