idris

2열

1답변

Idris가 Data.Vect의 인수를 크기와 항목 유형으로 정렬하는 이유는 무엇입니까?

제목과 마찬가지로 말입니다. (Agda와 Coq)에 익숙한 다른 종속 시스템에서 벡터 유형은 Vect : Type -> Nat -> Type으로 정의됩니다. 색인 앞에 매개 변수를 두는 것이 나에게 의미가 있으며, 어쨌든 벡터 유형의 표준 인 것처럼 보입니다. Idris가 왜 Vect : Nat -> Type -> Type을 사용합니까?

2열

1답변

Idris에서 x == y = p (x) == p (y)의 일반적인 개념을 정의 할 수 있습니까?

도메인 유형 t2에 p으로 투영하여 유형 랩퍼를 사용하여 도메인 유형 t1에 평등을 정의하는 개념을 구현하는 유형 생성자를 정의하고자합니다. data Projected : t1 -> t2 -> (p: t1 -> t2) -> Type where Project : t1 -> Projected t1 t2 p Projected_equals : Proj

1열

1답변

유형의 이름 - 이유는 무엇입니까?

는 사람이 나에게 설명 할 수이 왜 "t"는 여기 singleton : (t : Type) -> t -> HList [t] 을 사용합니까? t은 인스턴스 (Type)을 말합니까? 그러나 단순히이 작업을 수행 할 이유 : singleton : Type -> Type -> HList [Type]

4열

1답변

Idris 대화식에서이 재귀 함수를 어떻게 평가합니까?

이드리스로 물속에 잠기다, 나는 이드리스에게 this Haskell function을 이식하려고했다. 내가 대화 형 이드리스에서 그것을 호출 할 때 windowl : Nat -> List a -> List (List a) windowl size = loop where loop xs = case List.splitAt size xs of

1열

2답변

Idris의 상수

Idris에서 다른 언어로 상수라고 부르는 것을 정의하는 관용구적인 방법은 무엇입니까? 이거 야? myConstant : String myConstant = "some_constant1" myConstant2 : Int myConstant2 = 123 그렇다면, REPL에서 나는 선언 후 예외를 얻을 : 전역 상수를 선언 특별 (input):1

2열

1답변

스트림의 요소에 대한 완전 함 및 검색

Lists 및 Vect의 찾기 기능과 유사한 크기 제한 유형의 스트림에 대해 find 함수를 원합니다. total find : MaxBound a => (a -> Bool) -> Stream a -> Maybe a 도전 그것을 확인하는 것이다 는 는 N 최대 a을 인코딩하는데 필요한 비트 수를 넘지 상수 log_2 N 공간을 소비하지 총 수. 에는 런

3열

1답변

Idris의 유리수 구현

Idris에 유리수가 이미 구현되어 있습니까? 예. Haskell의 Data.Ratio 포트.

1열

1답변

날짜를 계산할 때 Fin n 및 Integer를 올바르게 처리하는 방법은 무엇입니까?

Idris를 탐구하는 여정에서 작은 날짜 처리 모듈을 "관용적 인"방식으로 작성하려고합니다. 여기까지 내가 지금까지 가지고있는 것이있다. module Date import Data.Fin Day : Type Day = Fin 32 data Month : Type where January : Month February : Mon

4열

1답변

쌍 (x/y)에 대한 유형 (x/= y)

(x, y) 쌍의 유형을 x /= y으로 설정하고 싶습니다. 내 생각은 NEqPa : Type -> Type는 NEqPa a이 x : a, y : a 및 p : (x = y) -> Void 모든 요소를 ((x,y), p) 포함한다고 정의하는 것입니다. 나는 다음과 같은 두 가지 버전을 시도 : NEqPa a = ((x, y) : (a, a) ** (x

12열

1답변

idris에 스트림의 필터 기능이없는 이유는 무엇입니까?

목록에는 filter : (a -> Bool) -> List a -> List a이 있지만 스트림에는 filter : (a -> Bool) -> Stream a -> Stream a이 없으므로 그 이유는 무엇입니까? 유사한 작업을 수행 할 수있는 대안이 있습니까? 이드리스에서