lean4-htt/tests/lean/run/float_cases_bug.lean
Leonardo de Moura a4c69ec32c chore: fix tests
2020-10-24 16:46:21 -07:00

4 lines
77 B
Text

new_frontend
def foo (xs : List Nat) :=
xs.span (fun n => (decide (n = 1)))