How to create a new type from string?

Stream: new members

[Colin Jones ⚛️]

How do I create a particular type using a string?

For example, I want to create a type that would encompass all possible 3 letter long strings that contain the letters "A", "B", and "C". Let's name this type three_letter.

"AAA" would be a three_letter
"ABC" would be a three_letter
"DDD" would not be a three_letter
"A" would not be a three_letter

[Damiano Testa]

You could do this:

def ABC := { s : String // s.length == 3 && s.dropWhile "ABC".toList.contains == "" }

example : ABC := ⟨"AAA", by rfl⟩

example : ABC := ⟨"ABC", by rfl⟩

example (a : ABC) (h : a.val = "A") : False := by
  have : "A".length = 1 := by rfl
  rcases a with ⟨a, ha⟩
  subst h
  simp_all

example (a : ABC) (h : a.val = "DDD") : False := by
  have : "DDD".dropWhile "ABC".toList.contains = "DDD" := by rfl
  rcases a with ⟨a, ha⟩
  subst h
  simp_all

[Colin Jones ⚛️]

Thank you

[Colin Jones ⚛️]

Does this make "AAA" as type ABC or does the first example just prove "AAA" is in the set ABC.

[Colin Jones ⚛️]

I would like to change "AAA" into type ABC if possible aka #check "AAA" outputs ABC

[Damiano Testa]

For that, you should make it a def and assign it a name. For instance

def aaa : ABC := ⟨"AAA", by rfl⟩

#check aaa

[Colin Jones ⚛️]

Okay, is there a way to transfer between types e.g. #check ("AAA" : ABC) like #check (1 : ℤ).

[Damiano Testa]

I don't think that you can: somewhere there has to be a check that the string that you are using satisfies your predicate.