regexp-test.why 266 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
theory Test

  clone import 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