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

Question

두 가지 자연스러운 주장을 취하고 어쩌면 평등성을 증명하는 함수를 작성하고 싶습니다.

나는

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) 
equal a b = case (a == b) of 
    True => Just Refl 
    False => Nothing 

으로 노력하고 있지만 다음과 같은 오류이 작업을 수행하는 올바른 방법입니다

When checking argument x to constructor Prelude.Maybe.Just: 
     Type mismatch between 
       True = True (Type of Refl) 
     and 
       Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == a 
                        b = 
       True (Expected type) 

     Specifically: 
       Type mismatch between 
         True 
       and 
         Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == a 
                          b 

를 얻을?

또한, 보너스 질문으로, 내가 할 경우

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) 
equal a b = case (a == b) of 
    True => proof search 
    False => Nothing 

나는

INTERNAL ERROR: Proof done, nothing to run tactic on: Solve 
pat {a_504} : Prelude.Nat.Nat. pat {b_505} : Prelude.Nat.Nat. Prelude.Maybe.Nothing (= Prelude.Bool.Bool Prelude.Bool.Bool (Prelude.Interfaces.Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == {a_504} {b_505}) Prelude.Bool.True) 
This is probably a bug, or a missing error message. 
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues 

는 알려진 문제입니다 얻거나 나는 그것을보고해야합니까?

Answer 1

의이 Nat의 Eq 인터페이스의 구현을 살펴 보자 :

Eq Nat where 
    Z == Z   = True 
    (S l) == (S r) = l == r 
    _ == _   = False 

당신은 문제를 해결할 수 있습니다 단지 (==) 함수의 구조에 따라 다음과 같이

total 
equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) 
equal Z Z = Just Refl 
equal (S l) (S r) = equal l r 
equal _ _ = Nothing 

Answer 2

당신을 case (종속 패턴 일치) 대신 with을 사용하면됩니다.

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) 
equal a b with (a == b) 
    | True = Just Refl 
    | False = Nothing 

Anton는 지적한 바와 같이 부울 테스트 결과에 대한 증인 일 뿐이며 적절한 평등보다 약한 주장입니다. if a==b then ...에 대한 증빙 자료를 제출하는 것이 유용 할 수 있지만 b 대신 a을 사용할 수 없습니다.