examples/tests/regexp-test.why

   1 theory Test
   2
   3   use seq.Seq
   4   clone regexp.Regexp with type char = int
   5
   6   lemma empty_is_empty: forall w: word. not (mem w Empty)
   7
   8   constant a: int = 0
   9   constant b: int = 1
  10   constant c: int = 2
  11
  12   goal G: mem (cons a (cons b empty)) (Concat (Char a) (Star (Char b)))
  13
  14 end
  15