blob: c71f884c30b464e280c1fbff27ae4d3663cd2670 [file] [edit]
def foo {α β : Type} (xs : Array (α × β)) (H : true = xs.all fun (x, y) => true) : Unit := ()