Besides, I don’t think your original goal is true: the variable L is free in
LHS, but bound in RHS, as shown in different colors.
Chun
Inviato da iPhone
> Il giorno 26 ott 2019, alle ore 17:18, Yassmeen Derhalli
> ha scritto:
>
>
> Dear Thomas,
>
> Thank you so much for your elaborated re
Dear Thomas,
Thank you so much for your elaborated reply.
I will go through Section 5.5.1.1 that you referred to
Thanks again!
Yassmeen
On Fri, Oct 25, 2019 at 1:22 PM Thomas Tuerk
wrote:
> Dear Yassmeen,
>
> set comprehensions in HOL are a bit cryptic. They are explained in Section
> 5.5.1
Dear Yassmeen,
set comprehensions in HOL are a bit cryptic. They are explained in
Section 5.5.1.1 of the Description manual. In short, something like {t |
p} is syntactic sugar that is turned by the parser into GSPEC(\(x1
,...,xn). (t,p)). The trick is figuring out, which variables x1, ... xn
to u
Hi,
I have this proof goal, where I need to prove that two sets are equal.
{{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
a |
a IN if j IN L then s3 j else s4 j} =
{{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
a IN if j IN L then s3 j el
