import logic data.num
open num
notation `o` := (10:num)
check 11
constant f : num → num
check o + 1
check f o + o + o
eval 9 + (1:num)
eval o+4