如何处理Agda不确定是否在`with`语句中生成构造函数case?

问题描述

我有以下代码:

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)

不幸的是，emacs 中的 Agda加载文件"命令失败并显示以下消息:

Unfortunately, Agda "load file" command in emacs fails with the following message:

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' 是一个常量，并且不确定 n 是否有任何先决条件总是小于 primCharToNat '9' (57).因此，不确定它是否应该生成 less 情况(我认为 equal 情况也是如此).我可以以某种方式强制 Agda 生成所有案例吗?

As far as I understand, Agda understands that primCharToNat '9' is a constant and is not sure whether there are any preconditions on n being always less than primCharToNat '9' (57). Therefore, it is not sure whether it should generate the less case (I assume it's also the case with equal case). Can I somehow force Agda into generating all cases?

背景:我正在尝试编写一个 digit : Char → Maybe ℕ 函数，如果传递的字符是十进制数字或 just x>nothing 如果不是.我考虑以下算法:使用 primCharToNat 将参数转换为自然数(可能是 ASCII 码)，然后将其与 primCharToNat '0' 和 primCharToNat 进行比较'9'.

Background: I'm trying to write a digit : Char → Maybe ℕ function which should return either just x if the character passed is a decimal digit or nothing if it's not. I think about the following algorithm: convert the argument to a natural number (ASCII code, probably) with primCharToNat and then compare it with primCharToNat '0' and primCharToNat '9'.

推荐答案

一个可能的解决方案是对 primCharToNat '9' 进行抽象:

A possible solution consists in abstracting over primCharToNat '9':

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

这篇关于如何处理Agda不确定是否在`with`语句中生成构造函数case?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！