是否可以在模式与它们匹配之前检查两个字符串的长度？

发布于 2025-01-29 06:52:48 字数 346 浏览 2 评论 0原文

我正在COQ中编程，并希望通过首先检查两个字符串的长度来消除非排量的案例匹配，例如，

Definition foo (word1 word2 : word) : option :=
    if length word1 =? length word2 then
    * pattern matching logic that only concerns same length word patterns *
    else None.

我仍然会遇到一个非避免的模式匹配错误。 M是否可以这样做，还是我必须以另一种方式处理我的功能？

原文

I'm programming in Coq and want to eliminate non-exhaustive case matching by checking the length of the two strings first, for example

Definition foo (word1 word2 : word) : option :=
    if length word1 =? length word2 then
    * pattern matching logic that only concerns same length word patterns *
    else None.

I still get a non-exhaustive pattern matching error. Is it possible for m to do this or do I have to approach my function in another way?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

云淡月浅 2025-02-05 06:52:48

总有选项在结尾添加通配符匹配语句以抑制该错误。假设您可以将其从OCAML转移到Coq，这是我的意思：

let foo x y =
    if String.length x = String.length y
    then
       match (x,y) with
       | ("foo","bar") -> Some true
       | _ -> None
    else
       None

使用通配符时，可以删除周围环境，如果是因为通配符箱也捕获了不同的长度字符串。

There is always the option to add a wildcard match statement at the end to suppress that error. Assuming, you can transfer this from ocaml to coq, here is what I mean:

let foo x y =
    if String.length x = String.length y
    then
       match (x,y) with
       | ("foo","bar") -> Some true
       | _ -> None
    else
       None

When using the wildcard, you can remove the surrounding if, of course, because the wildcard case also catches different length strings.

回复收藏 0 原文

~没有更多了~