CakeML/cakeml

Add contains to Char module

开放

#1,433 创建于 2026年7月18日

 (0 条评论) (0 个反应) (0 位负责人)Standard ML (98 个派生)auto 404
basis extensionsgood first issuelow effort

仓库指标

星标
 (1,169 个星标)
PR 合并指标
 (PR 指标待抓取)

描述

It would be useful to have Char.contains in part of the basis. One simple implementation is the following:

fun contains s c = List.member c (String.explode s)

However, I would suspect that it would be better to avoid the explode and iterate over the string instead for the definition that ends up being translated. It might be neat to prove a theorem of equivalence between them, though.

贡献者指南