Idris - 모듈에서 가져온 경우 표현식이 수행되지 않습니다.

Question

특정 유형/조건부 IsSet 및 결정 성 기능 isSet을 정의하는 Idris 모듈이 있습니다. 또한 IsSet이라는 증명을 얻기 위해 유형 확인시 해당 결정 가능성 함수를 계산하는 몇 가지 도우미 함수를 정의합니다.

Test1.idr

module Test1 

import Data.List 

%default total 
%access export 

data IsSet : List t -> Type where 
    IsSetNil : IsSet [] 
    IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs) 

ifNotSetHereThenNeitherThere : Not (IsSet xs) -> Not (IsSet (x :: xs)) 
ifNotSetHereThenNeitherThere notXsIsSet (IsSetCons xIsInXs xsIsSet) = notXsIsSet xsIsSet 

ifIsElemThenConsIsNotSet : Elem x xs -> Not (IsSet (x :: xs))  
ifIsElemThenConsIsNotSet xIsInXs (IsSetCons notXIsInXs xsIsSet) = notXIsInXs xIsInXs 

isSet : DecEq t => (xs : List t) -> Dec (IsSet xs) 
isSet [] = Yes IsSetNil 
isSet (x :: xs) with (isSet xs) 
    isSet (x :: xs) | No notXsIsSet = No $ ifNotSetHereThenNeitherThere notXsIsSet 
    isSet (x :: xs) | Yes xsIsSet with (isElem x xs) 
    isSet (x :: xs) | Yes xsIsSet | No notXInXs = Yes $ IsSetCons notXInXs xsIsSet 
    isSet (x :: xs) | Yes xsIsSet | Yes xInXs = No $ ifIsElemThenConsIsNotSet xInXs 

getYes : (d : Dec p) -> case d of { No _ =>(); Yes _ => p} 
getYes (No _) =() 
getYes (Yes prf) = prf 

getNo : (d : Dec p) -> case d of { No _ => Not p; Yes _ =>()} 
getNo (No cnt) = cnt 
getNo (Yes _) =() 

setTest1 : IsSet ["x"] 
setTest1 = getYes $ isSet ["x"] 

: 내가 다른 파일에 정의하고 내가 원래 모듈을 가져올 때 모듈 내부에 제대로 보조 기능의 유형 체킹 것을 사용하지만, 그렇지 않은

표현 Test2.idr

module Test2 

import Test1 

%default total 
%access export 

setTest2 : IsSet ["x"] 
setTest2 = getYes $ isSet ["x"] 

setTest1 typechecks 올바르게하지만 setTest2 다음과 같은 오류가 발생합니다 :

When checking right hand side of setTest2 with expected type 
     IsSet ["x"] 

Type mismatch between 
     case block in getYes at Test1.idr:26:30 (IsSet ["x"]) 
               (isSet ["x"]) 
               (isSet ["x"]) (Type of getYes (isSet ["x"])) 
and 
     IsSet ["x"] (Expected type) 

I 유형은 Test2.idr를 확인해 볼 때 (다만 종류에 반대)

Answer 1

이

가, 유형 검사는 정의을 모르는 이드리스 0.12를 사용하고 있습니다를 isSet이므로 형식 서명을 getYes으로 줄일 수 없으므로 형식이 일치하지 않습니다. 이 작업을 수행하려면 isSet의 public export을 사용해야합니다. Idris의 공개 규칙으로 인해 isSet은 (현재 내보내지지 않은) 정의를 참조하기 때문에 public exportIsSet 유형이 있어야합니다.

이가없이 때문에,하지만, 어쨌든 아마 좋은 생각이다, 그 모듈이 정의를 알고하지 않기 때문에 Test2.idr에서

isNil : IsSet l -> Bool 
isNil IsSetNil = True 
isNil (IsSetCons f y) = False 

데이터 생성자, 즉, 일하는 것이

같은조차 간단한 함수, 유형의.