CakeML/cakeml

Add contains to Char module

Ouverte

#1 433 ouverte le 18 juil. 2026

 (0 commentaire) (0 réaction) (0 personne assignée)Standard ML (98 forks)auto 404
basis extensionsgood first issuelow effort

Métriques du dépôt

Stars
 (1 169 étoiles)
Métriques de merge PR
 (Métriques PR en attente)

Description

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.

Guide contributeur