How would you make a type for alphanumeric characters?

Stream: general

[nrs]

How would you make a type for alphanumeric characters, without manually enumerating each character? (e.g. inductive AlNum | a | b | .... Maybe there is a way to make an inductive type with constructorChar -> Type that supplies a default proof?

[Henrik Böving]

The easiest approach is most likely a subtype that carries a proof that the character is within the ASCII alpha numeric ranges

[nrs]

Henrik Böving said:

The easiest approach is most likely a subtype that carries a proof that the character is within the ASCII alpha numeric ranges

Hm, a record with two fields, one containing a string and the other the proof? If so, is there a way to provide some sort of default proof?

[Henrik Böving]

Sure := by tactic

[nrs]

ah very nice! thanks a lot for the idea, here's a working implementation:

structure alphaNum where
  char : Char
  prop : char.isAlphanum = true := by trivial

def an1 : alphaNum := .mk 'a'
def an7 : alphaNum := .mk '7'

I guess the challenge isn't so much in defining the type but in making helper functions that ease working with it