idris

3열

1답변

Type Constructor 매개 변수에 대한 인터페이스 제약 조건이있는 Idris 종속 레코드

idris에서 종속 레코드의 형식 생성자에 대한 매개 변수에 대한 인터페이스 제약 조건을 사용할 수 있습니까? 인터페이스가 Show : Type -> Type입니다. 지금은 다음에 의존 기록에 제약을 줄 필요가 : record Source s where constructor MkSource initial : s 내가 항상 Show의 인

4열

2답변

이드리스 -

한다고 가정 열거 형에 대한 식 나는 data MyType = One | Two | Three ... | Ten 같은 열거 형을 가지고 있고 나는 그것을 위해 Eq 인터페이스를 구현하고 싶습니다. 나는 다음과 같이 할 수있다. Eq MyType where One == One = True Tw

2열

1답변

다음 코드는 출신 유도 정의 형

(https://stackoverflow.com/a/37461290/2129302)에 대한 구현 (쇼를) 찾기 : mkStr : (Show a) => tensor shape a -> String mkStr x = show x 하지만 그 대신이 : tensor : Vect n Nat -> Type -> Type tensor [] a = a tens

2열

1답변

재귀 유형의 중첩 생성자 내부에있는 증명

아래 코드를 사용하는 데 문제가 있습니다. 본질적으로 슬라이스 유형을 만들고 싶습니다. 동기 부여는 Python에서 이루어지며 슬라이스는 [start:end:step]이며 목록에서 하위 목록을 분할하는 데 사용됩니다. 이것은 개념적으로 일련의 인덱스 인 [start, start+step, start+2*step, ..., end]과 같습니다. 캡처하려고 시

4열

1답변

이드리스은 - 다음 I가 이드리스에서 N 차원 벡터를 정의

막내 차원 벡터에 대해 작업을 매핑 : import Data.Vect NDVect : (Num t) => (rank : Nat) -> (shape : Vect rank Nat) -> (t : Type) -> Type NDVect Z [] t = t NDVect (S n) (x::xs) t = Vect x (NDVect n xs t) 그러면 I

2열

2답변

이드리스 (Idris) - 두 숫자의 동등성 확인

두 가지 자연스러운 주장을 취하고 어쩌면 평등성을 증명하는 함수를 작성하고 싶습니다. 나는 equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) equal a b = case (a == b) of True => Just Refl False => Nothing 으로 노력하고 있지만 다음과

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

0열

1답변

이드리스 - 평등 주장은 구현이 그와 관련이없는 경우에도,

는 다음과 같은 기능을 고려하시기 바랍니다 실패 : 나는 REPL에서 vectTranspose을 계산하려고하면 예상대로 vectTranspose : Vect n (Fin 3) -> Vect 3 (List (Fin n)) vectTranspose {n = Z} [] = [[],[],[]] vectTranspose {n = (S len)} (x :: xs)

4열

1답변

모델없이 Idris에 물건을 증명할 방법이 있습니까?

필자는 Hilbert 평면에 대한 기하학에서 발생 빈도를 구현하려고 노력해 왔습니다. 그리고 다음과 같은 공리를 내놓았습니다. interface (Eq point) => Plane line point where -- Abstract notion for saying three points lie on the same line. colinea

0열

1답변

`replace`를 통해 이러한 commutativity의 증명을 완성하는 방법은 무엇입니까?

this 설명서에는 증명을 완료하는 데 replace을 사용할 수있는 방법이 나와 있지만 rewrite으로 끝나며 이는 replace이라고 쓰는 구문 설탕처럼 보입니다. 나는 그것을 명시 적으로 사용하는 방법을 이해하는데 관심이있다. 정확하게 이해하면 S k = S (plus k 0)을 S (plus k 0) = S (plus k 0)으로 다시 쓸 수 있으