19 lines
717 B
Text
19 lines
717 B
Text
fn is_pangram{n:nat}(s: string(n)): bool = loop(s, i2sz(0)) where {
|
|
val letters: arrayref(bool, 26) = arrayref_make_elt<bool>(i2sz(26), false)
|
|
fn check(): bool = loop(0) where {
|
|
fun loop{i:int | i >= 0 && i <= 26}(i: int(i)) =
|
|
if i < 26 then
|
|
if letters[i] then loop(i+1) else
|
|
false
|
|
else true
|
|
}
|
|
fun add{c:int}(c: char(c)): void =
|
|
if (c >= 'A') * (c <= 'Z') then letters[char2int1(c) - char2int1('A')] := true else
|
|
if (c >= 'a') * (c <= 'z') then letters[char2int1(c) - char2int1('a')] := true
|
|
fun loop{i:nat | i <= n}.<n-i>.(s: string(n), i: size_t(i)): bool =
|
|
if string_is_atend(s, i) then check() else
|
|
begin
|
|
add(s[i]);
|
|
loop(s, succ(i))
|
|
end
|
|
}
|