How do I prove that c-'a' is within [0,26)?

Suppose I have this code:

#include "share/atspre_staload.hats"

val letters = arrayref_make_elt<bool>(i2sz(26), false)

implement main0() =
  begin
    println!("found('a'): ", letters[0]);
    println!("found('f'): ", letters[5]);
  end

Which produces the output:

found('a'): false
found('f'): false

I'd like to index into letters by character, instead. Actually, given any character I'd like to index into letters only if it's a valid index.

So this almost works:

#include "share/atspre_staload.hats"

val letters = arrayref_make_elt<bool>(i2sz(26), false)

typedef letter = [c:int | c >= 'a' && c <= 'z'] char(c)
typedef letteri = [i:int | i >= 0 && i < 26] int(i)

(* fn letter2index(c: letter): letteri = c - 'a' *)  (* #1 *)

fn letter2index(c: letter): letteri =
  case- c of
  | 'a' => 0
  | 'f' => 5

fn trychar(c: char): void =  (* #2 *)
  if c >= 'a' && c <= 'z' then
    println!("found('", c, "'): ", letters[letter2index(c)])

implement main0() =
  begin
    trychar('a');
    trychar('f');
    trychar('+');  (* #3 *)
  end

If I change char to letter at #2 and remove trychar('+') at #3, then this compiles. But of course I'd rather perform subtraction at #1 rather than have a big case of letters, and I'd to apply trychar to any kind of char, not just a letter.

The code you want can be written as follows:

#include
"share/atspre_staload.hats"

stadef
isletter(c:int): bool = ('a' <= c && c <= 'z')

val
letters = arrayref_make_elt<bool>(i2sz(26), false)

fn
letter2index
{ c:int
| isletter(c)}
(c: char(c)): int(c-'a') = char2int1(c) - char2int1('a')

fn
trychar
{c:int}
(c: char(c)): void =
if
(c >= 'a') * (c <= 'z')
then
println!("found('", c, "'): ", letters[letter2index(c)])

implement main0() =
begin
  trychar('a');
  trychar('f');
  trychar('+');
end

In your original code, quantifiers (forall and exists) were not used correctly.