Agda 使用以下运算符来显示集合之间的逆:
_↔_ : ∀ {f t} → Set f → Set t → Set _
idris 有等价物吗?我正在尝试在列表上定义包相等
data Elem : a -> List a -> Type where
Here : {xs : List a} -> Elem x (x :: xs)
There : {xs : List a} -> Elem x xs -> Elem x (y :: xs)
(~~) : List a -> List a -> Type
xs ~~ ys {a} = Elem a xs <-> Elem a ys
这样我们就可以构造
l1 ~~ l2
当l1
和 l2
以任何顺序具有相同的元素。Agda definition of
↔
似乎非常复杂,我不确定 Idris 标准库中是否有等效的东西。
最佳答案
Agda 背后的基本思想 ↔
是用两个往返证明打包两个函数,这在 Idris 中也很容易做到:
infix 7 ~~
data (~~) : Type -> Type -> Type where
MkIso : {A : Type} -> {B : Type} ->
(to : A -> B) -> (from : B -> A) ->
(fromTo : (x : A) -> from (to x) = x) ->
(toFrom : (y : B) -> to (from y) = y) ->
A ~~ B
您可以像在以下最小示例中一样使用它:
notNot : Bool ~~ Bool
notNot = MkIso not not prf prf
where
prf : (x : Bool) -> not (not x) = x
prf True = Refl
prf False = Refl
Agda 版本更复杂的原因是因为它也对等式的选择进行了参数化,因此它不必是命题(这是最严格/最好的)。参数化
~~
的 Idris 定义以上来自 =
到任意PA : A -> A -> Type
和 PB : B -> B -> Type
留给读者作为练习。
关于list - idris 有没有相当于 Agda 的 ↔,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/27276081/