`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「ロード・ファイルは、」emacsの中のコマンドは、次のメッセージで失敗しますの前提条件が常にprimCharToNat '9'（57）未満であるかどうかは不明です。したがって、lessケースを生成するかどうかはわかりません（equalの場合もそうです）。私はどういうわけかAgdaにすべての症例を生成させることができますか？

背景：私はjust xの文字が小数点の桁である場合は、そうでない場合はnothingのいずれかを返さなければなりません。私は次のアルゴリズムについて考えます：primCharToNatで引数を自然数（おそらくASCIIコード）に変換してからprimCharToNat '0'とprimCharToNat '9'と比較してください。

Answer 1

可能な解決策は、primCharToNat '9'上に抽象化することからなる：

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