我怎样才能改变 forall 在 agda 中的工作？

Question

我正在使用一对有理数流，假设 (L,R) 其中 L 和 R 是有理数流。 L 和 R 都必须满足 3 个条件才能说它有效。我把代码写成..

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 ⊥

我很想把这个函数的return类型改成Bool。这里 cut 表示 (L, R) 而 mem 是成员资格。

问题来自 forall p q which expect return type to be Set。我应该如何处理才能获得理想的结果。

Answer 1

你可以这样写：

isCut : cut → (p q : pair) → Bool
isCut x p q = (((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))))

我怎样才能改变 forall 在 agda 中的工作？

How can i change working of forall in agda?

agda