regexp-test.why

theory Test

  clone regexp.Regexp with type char = int

  lemma empty_is_empty: forall w: word. not (mem w Empty)

  constant a: int = 0
  constant b: int = 1
  constant c: int = 2

  goal G: mem (Cons a (Cons b Nil)) (Concat (Char a) (Star (Char b)))

end