axiom val : nat

definition foo : nat :=
val

noncomputable definition foo2 : nat :=
val

definition bla : nat :=
2
