fact: Definition spec : ADT sig := Def ADT { rep := (list data), Def Constructor0 "empty" : rep := ret nil,, Def Method1 "enqueue" (self : rep) (d : data) : rep := ret (self ++ d :: nil), Def Method0 "dequeue"(self : rep) : rep * (option data) := match self with | nil => ret (self, None) | d :: self' => ret (self', Some d) end }.
imports: Tutorial