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.

貢獻者指南