[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: id resolution



Borzoo,

> IF (EXISTS (s0, s1:(S)): member(s1, ms)) THEN
>          fpcal (add(s0, ms))
> ELSE ms
>
> the type checker complains about the resolution of "s0" in
> "add(s0, ms)".  Is there anyway to resolve this without
> defining a variable?

The reference to s0 in the THEN part of the IF-THEN-ELSE
expression is not in the scope of the existential quantifier that
binds the variables s0 and s1 in the conditional part. In order
to refer to s0 in the THEN part you need to introduce the
variable through a binding operator either within the THEN part,
or outside the IF-THEN-ELSE expression.

	- Holger