Definition foo (x : nat) := Eval native_compute in x.