erg/tests/not_yet/dependent.er
2023-01-07 20:04:35 +09:00

16 lines
424 B
Python

Queue! T: Type, N: Nat! = Class {.payload = [T; !N]}
Queue!.
new = Self!(*, 0)::__new__ {.payload = []}
Queue!(T, N).
enqueue!(ref!(self(T, N ~> N+1)), x: T) =
self.payload.push! x
dequeue!(ref! self(T, N ~> N-1)): T =
self.payload.remove!(0)
q = Queue!.new()
q.enqueue!(1)
q.enqueue!(2)
q: Queue!(Int, !2)
assert q.dequeue!() == 1
assert q.dequeue!() == 2
# q.dequeue!() will cause a TypeError