I am working with pair of Stream of rationals, Lets say (L,R) Where L and R are Stream of rationals. There are 3 conditions which L and R both have to satisfy to say it is valid. I have written the code as..
isCut_ : cut → Set
isCut x = (p q : pair ) →
if((((p mem (getLC x)) ∨ (p mem (getRC x)))) ∧
((not (p mem getLC x)) ∨ (not (p mem getRC x))) ∧
(not (p <pair q) ∨ ((p mem getLC x) ∨ (q mem getRC x))))then ⊤
else ⊥
I really wanted to change the return type of this function to Bool. Here cut means (L, R) and mem is membership.
The problem coming from forall p q which expect return type to be Set
.
How should i handle to get desired result.
You can write something like this: