idris

8热度

1回答

我如何让Idris自动证明两个值不相等？

我如何让Idris自动证明两个值不相等？ p : Not (Int = String) p = \Refl impossible 我该如何让Idris自动生成此证明？ auto似乎不能证明涉及Not的陈述。我的最终目标是让Idris自动证明矢量中的所有元素都是唯一的，并且两个矢量不相交。 namespace IsSet data IsSet : List t -> Type whe

proof idris 2017-09-30

---

2热度

1回答

这个'with'块为什么会破坏这个函数的整体性？

我试图计算奇偶校验与半的地板一起，在自然数： data IsEven : Nat -> Nat -> Type where Times2 : (n : Nat) -> IsEven (n + n) n data IsOdd : Nat -> Nat -> Type where Times2Plus1 : (n : Nat) -> IsOdd (S (n + n)) n

idris termination totality 2017-10-04

---

3热度

1回答

伊德里斯改写不会发生

import Data.Vect import Data.Vect.Quantifiers sameKeys : Vect n (lbl, Type) -> Vect n (lbl, Type) -> Type sameKeys xs ys = All (uncurry (=)) (zip (map fst xs) (map fst ys)) g : {xs,ys : Vect n (

idris 2017-10-04

---

4热度

1回答

伊德里斯 - 感性步

证明考虑下面的函数 tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) tryMove Z from to [] = Nothing tryM

idris 2017-10-06

---

1热度

1回答

如何在Idris中编写一个非常懒惰的版本？

inf : Nat inf = S inf minimum' : Lazy Nat -> Lazy Nat -> Lazy Nat minimum' Z b = Z minimum' b Z = Z minimum' (S a) (S b) = S (minimum' a b) main : IO() main = do print $ Force $ minimum'

idris 2017-10-10

---

6热度

1回答

为什么idris中的这两个元组相等？

我读Type driven development with Idris，和的一个练习要求读者限定，使得随着一个矢量可以表示一个类型TupleVect，： TupleVect 2 ty = (ty, (ty,())) 我解决它通过定义以下类型： TupleVect : Nat -> Type -> Type TupleVect Z ty =() TupleVect (S k) ty = (

idris 2017-10-19

---

3热度

1回答

伊德里斯 - 懒惰的评价问题

考虑此程序： module test import Effects import Effect.StdIO (>>==) : Maybe a -> Lazy (a -> Maybe b) -> Maybe b (>>==) Nothing (Delay map) = Nothing (>>==) (Just x) (Delay map) = map x nothing : Str

monads lazy-evaluation idris 2017-10-19

---

2热度

1回答

隐式参数的顺序如何影响idris？

这种失败： > the ({A : Type} -> A -> {B : Type} -> B -> (A, B)) MkPair (input):1:5:When checking argument value to function Prelude.Basics.the: Type mismatch between A -> B1 -> (A, B1) (Type

idris 2017-10-21

---

1热度

1回答

难度在伊德里斯

我试图在我的定义的数据类型中的一种证明属性如下应用证明： reverseProof' : (inputBlock : Block iType iSize iInputs) -> (ind : Fin rSize) -> (rInputs : Vect rSize Ty) -> (receiveBlock : Block rType rSize rInput

idris theorem-proving 2017-09-11

---

3热度

1回答

伊德里斯：在记​​录隐参数

当我尝试编译这个例子 record R where f:() -> {t: Type} -> t 我得到这个错误： Type mismatch between () -> t1 (Type of f) and () -> t (Expected type) Specifically: Type mismatch between

idris 2017-09-16

---