함수 내부에서 암시 적 변수를 사용하려면 어떻게해야합니까? dim : Vect n a -> Nat
dim vec = n
를 오류받지 않고 : When elaborating right hand side of rep:
No such variable n
내부에서이 값에 액세스 할 수있는 방법이 있나요을 가장 단순한 경우에 감소, 그것을 가질 수 있습니
저는 최근에 직장에서했던 것들을 (더 간단한 방법으로) 재구성하여 Idris를 배우려고합니다. 크레딧 벡터 및 차변 벡터를 사용하여 일반 원장을 모델링하는 데이터 유형을 갖고 싶습니다. 나는 이것을 멀리까지 얻었습니다 : data GL : Type where
MkGL : (credits : Vect n Integer) ->
(debits : V
Idris/Haskell에서는 타입에 주석을 달고 Vect와 같은 GADT 생성자를 사용하여 데이터의 속성을 증명할 수 있지만이 경우 유형에 속성을 하드 코딩해야합니다 (예 : Vect 리스트와는 다른 타입이어야한다). 생성자에 과부하가 걸리거나 효과의 정맥에 무언가를 사용하는 것과 같이 열려있는 속성 집합 (예 : 길이 및 실행 평균을 모두 포함하는 목록
, 하나는 쓸 수있다 : containsTen::Num a => Eq a => [a] -> Bool
containsTen (x : y : xs)
| x + y == 10 = True
| otherwise = False
은 (위의 것보다 더 복잡 내 진짜 경우) ifThenElse으로 그 일을하지 않고, 이드리스에 상응하는 뭔가를 쓸
Type 1 인 주민의 예가 Type도 아니고 주민 번호가 Type도 아닌가? Idris REPL에서 탐험을하면서 나는 무엇이든 올 수 없었다. 가 더 정확하게하려면 , 나는 다음과 같은 산출이 Type 이외의 x을 찾고 있어요 : Idris> :t x
x : Type 1
I)가 작동하도록 Z 경우를 얻으려면. 유형 (j : Nat) -> {auto p : So (j < n)} -> Fin n의 이드리스 함수는 Fin n에 Nat을 변환 할 수 있도록 노력 (출력 FZ하고있어, 0 < n을 증명하는 것이 충분하다는 것을 증명하려고 노력하고 있습니다. 그러나 이것을 수행하는 방법을 배울 수는 없습니다. 나는 완전히 다른 기능을
저는 현재 cabal install idris을 통해 이드리스를 건축 중입니다. 출력에 대한 응답으로 : Redirecting build log to {handle:/home/me/.cabal/logs/idris-0.9.14.3.log}
tail -f /home/me/.cabal/logs/idris-0.9.14.3.log으로 빌드를 추적하기로 결정했습니
Idris에서 결정할 수있는 구문 분석기를 만들려고합니다. 처음에는 자연수를 파싱하는 것을보고 있었지만 예기치 않은 문제가 발생했습니다. 를 생성하는 코드의 최소한의 예는 이것이다 : data Digit : Char -> Type where
Zero : Digit '0'
One : Digit '1'
digitToNat : Digit a