19 Jun
2010
19 Jun
'10
12:09 p.m.
Hello, I tried to use the free theorem generator in order to check whether the only values of type `(Bool -> a) -> a` are `($True)` and `($False)`. However, I don't manage to interpret the result: forall t1,t2 in TYPES, g :: t1 -> t2. forall p :: Bool -> t1. forall q :: Bool -> t2. (forall x :: Bool. g (p x) = q x) ==> (g (f_{t1} p) = f_{t2} q) What are `f_{t1}` and `f_{t2}` ? Regards, Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)