2017-11-28 16 views
0

저는 이사벨에게 신입생이며 대학 운동을하고 있습니다. 이사벨의 역기능을 증명할 필요가있어.이사벨 유형 오류

하스켈에서 함수는 다음과 같을 것이다 : 지금 이자벨에서이 기능을 "회전"을 정의하는 tryed

rev [] = [] 
rev (x:xs) = rev xs ++ [x] 

.

Type unification failed: Clash of types "_ 
      ⇒ _" and "_ Exercise5.list" 

Type error in application: incompatible operand type 

Operator: app (rev xs) :: 
    'a Exercise5.list ⇒ 'a Exercise5.list 
Operand: Exercise5.list.Cons :: 
    ??'a ⇒ ??'a Exercise5.list ⇒ ??'a Exercise5.list 

경우 문제는 다음과 같습니다 유형 목록과 기능 "응용 프로그램"

function app and rev in Isabelle

이사벨이 나에게주는 오류를 (추가)? 내가 이해하는 한, Isabelle은 "어이 친구 앱에는 목록의 두 개의 인수가 필요하지만 여기서는 해당되지 않습니다"

왜 그런가요? xs은 분명히 유형 '목록이고 내 단점 연산자와 함께 x도 목록으로 만드시겠습니까?

감사합니다.

답변

1

괄호를 어디에 넣어야하는지 생각해보십시오. app rev xs Cons x Nil : 현재 Nil에 함수 x을 적용한 것 같습니다.

+0

감사합니다! 단점 (x nil)은 ** (단 x xil)이어야합니다. ** 그게 내 작은 문제를 해결했습니다. 감사 :) –