'with'문에서 생성자 케이스를 생성할지 여부에 대해 Agda를 다루지 않는 방법은 무엇입니까?

Question

나는 다음과 같은 코드가 있습니다 :

tmp.agda:7,1-8,12 
I'm not sure if there should be a case for the constructor less, 
because I get stuck when trying to solve the following unification 
problems (inferred index ≟ expected index): 
    m ≟ n 
    suc (m + k) ≟ 57 
when checking the definition of with-6 

지금까지 내가 이해, AGDA는 primCharToNat '9'이 인 것을 이해 :

open import Data.Nat 
open import Agda.Builtin.Char 
open import Data.Maybe 

digit' : ℕ → Maybe ℕ 
digit' n with compare n (primCharToNat '9') 
... | greater _ _ = nothing 
... | _ = ? 

digit : Char → Maybe ℕ 
digit c = digit' (primCharToNat c) 

불행하게도, AGDA "로드 파일은"이맥스의 명령은 다음과 같은 메시지와 함께 실패 상수이고 에 대한 전제 조건이 항상 primCharToNat '9' (57)보다 작은 지 여부는 확실하지 않습니다. 따라서 less 사례를 생성해야하는지 여부는 확실하지 않습니다 (이 경우 equal 경우도 있다고 가정합니다). 어떻게 든 Agda가 모든 케이스를 생성하도록 강요 할 수 있습니까?

배경 : 전달할 문자가 십진수이거나 그렇지 않으면 nothing 인 경우 just x을 반환해야하는 digit : Char → Maybe ℕ 함수를 작성하려고합니다. 나는 다음과 같은 알고리즘에 대해 생각해 보았다 : primCharToNat으로 인수를 자연수 (ASCII 코드)로 변환 한 다음 primCharToNat '0' 및 primCharToNat '9'과 비교한다.

Answer 1

가능한 용액으로 추출 이루어져 primCharToNat '9' 위에 :

digit' : ℕ → Maybe ℕ 
digit' n with primCharToNat '9' | compare n (primCharToNat '9') 
... | _ | greater _ _ = nothing 
... | _ | _ = {!!}